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

DOI10.1145/3209108.3209195zbMATH Open1453.03070OpenAlexW2799007918WikidataQ130855304 ScholiaQ130855304MaRDI QIDQ5145362FDOQ5145362

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

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

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)

Cited In (2)

• Monoidal-closed categories of tree automata
• Title not available (Why is that?)

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)