LMSO: a Curry-Howard approach to Church's synthesis via linear logic

DOI10.1145/3209108.3209195MaRDI QIDQ5145362zbMATH OpenOpenAlexWikidataFDO

Authors Pierre Pradic, Colin Riba

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209195

zbMATH Keywords

categorical logicgame semanticslinear logicrealizabilityMSO on infinite words

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• scientific article; zbMATH DE number 7204449
• scientific article; zbMATH DE number 7147442
• A Dialectica-like interpretation of a linear MSO on infinite words
• Logical Refinements of Church’s Problem
• Synthesis of functional programs with help of first-order intuitionistic logic

Cited in

(3)

• Monoidal-closed categories of tree automata
• scientific article; zbMATH DE number 7147442 (Why is no real title available?)
• A Dialectica-like interpretation of a linear MSO on infinite words

This page was built for publication: LMSO: a Curry-Howard approach to Church's synthesis via linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145362)