ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 16:30 - 17:10 at S3 - IV

We devise a variant of Dialectica interpretation of intuitionistic linear logic for LMSO, a linear logic-based version of MSO over infinite words. LMSO was known to be correct and complete with respect to Church’s synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of MSO on infinite words, our interpretation provides us with a syntactic approach, without any further construction of automata on infinite words. Via Dialectica, as linear negation directly corresponds to switching players in games, we furthermore obtain a complete logic: either a closed formula or its linear negation is provable. This completely axiomatizes the theory of the realizability model of LMSO. Besides, this shows that in principle, one can solve Church’s synthesis for a given \forall\exists-formula by only looking for proofs of either that formula or its linear negation.

Conference Day
Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change