A Curry-Howard Approach to Church's Synthesis

Autor: Pradic, Pierre, Riba, Colin
Přispěvatelé: Faculty of Mathematics, Informatics, and Mechanics [Warsaw] (MIMUW), University of Warsaw (UW), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Preuves et Langages (PLUME), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), ANR-14-CE25-0007,RAPIDO,Raisonner et Programmer avec des Données Infinies(2014), ANR-11-BS02-0010,RECRE,Réalisabilité pour la logique classique, la concurrence, les références et la réécriture(2011), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Riba, Colin, Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL)
Jazyk: angličtina
Rok vydání: 2018
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
000 Computer science
knowledge
general works
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES
010102 general mathematics
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Intuitionistic Arithmetic
0102 computer and information sciences
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic
01 natural sciences
Logic in Computer Science (cs.LO)
Realizability
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
Computer Science
Monadic Second-Order Logic on Infinite Words
0101 mathematics
Computer Science::Formal Languages and Automata Theory
Zdroj: FSCD'17
FSCD'17, Sep 2017, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2017.29⟩
DOI: 10.4230/LIPIcs.FSCD.2017.29⟩
Popis: Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic (MSO) over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, an intuitionistic variant of MSO over infinite words, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.
Databáze: OpenAIRE
Externí odkaz: