@inproceedings{10.1007/978-3-030-17127-8_27,
    Abstract = {We devise a variant of Dialectica interpretation of intuitionistic linear logic for , a linear logic-based version {\$}{\$}{\backslash}mathsf {\{}MSO{\}}{\$}{\$}over infinite words. was known to be correct and complete w.r.t. Church's synthesis, thanks to an automata-based realizability model. Invoking B{\"u}chi-Landweber Theorem and building on a complete axiomatization of {\$}{\$}{\backslash}mathsf {\{}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 . Besides, this shows that in principle, one can solve Church's synthesis for a given {\$}{\$}{\backslash}forall {\backslash}exists {\$}{\$}-formula by only looking for proofs of either that formula or its linear negation.},
    Address = {Cham},
    Author = {Pradic, Pierre and Riba, Colin},
    BookTitle = {Foundations of Software Science and Computation Structures},
    Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex},
    File = {Pradic-Riba2019\_Chapter\_ADialectica-LikeInterpretation (0) - a - a - b.pdf},
    ISBN = {978-3-030-17127-8},
    Pages = {470--487},
    Publisher = {Springer International Publishing},
    Title = {A Dialectica-Like Interpretation of a Linear MSO on Infinite Words},
    Year = {2019},
    date-added = {2019-04-11 15:31:37 +0200},
    date-modified = {2019-04-11 15:31:37 +0200},
    doi = {10.1007/978-3-030-17127-8_27}
}

@inproceedings{10.1007/978-3-030-17127-8_27, Abstract = {We devise a variant of Dialectica interpretation of intuitionistic linear logic for , a linear logic-based version {\$}{\$}{\backslash}mathsf {{}MSO{}}{\$}{\$}over infinite words. was known to be correct and complete w.r.t. Church's synthesis, thanks to an automata-based realizability model. Invoking B{\"u}chi-Landweber Theorem and building on a complete axiomatization of {\$}{\$}{\backslash}mathsf {{}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 . Besides, this shows that in principle, one can solve Church's synthesis for a given {\$}{\$}{\backslash}forall {\backslash}exists {\$}{\$}-formula by only looking for proofs of either that formula or its linear negation.}, Address = {Cham}, Author = {Pradic, Pierre and Riba, Colin}, BookTitle = {Foundations of Software Science and Computation Structures}, Editor = {Boja{\'{n}}czyk, Miko{{\l}}aj and Simpson, Alex}, File = {Pradic-Riba2019_Chapter_ADialectica-LikeInterpretation (0) - a - a - b.pdf}, ISBN = {978-3-030-17127-8}, Pages = {470--487}, Publisher = {Springer International Publishing}, Title = {A Dialectica-Like Interpretation of a Linear MSO on Infinite Words}, Year = {2019}, date-added = {2019-04-11 15:31:37 +0200}, date-modified = {2019-04-11 15:31:37 +0200}, doi = {10.1007/978-3-030-17127-8_27} }