Document Open Access Logo

Relational Semantics of Linear Logic and Higher-order Model Checking

Authors Charles Grellois, Paul-André Melliès

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.260.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Charles Grellois
Paul-André Melliès

Cite As Get BibTex

Charles Grellois and Paul-André Melliès. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 260-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.260

Abstract

In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic second-order logic for higher-order recursion schemes.

Subject Classification

Keywords
  • Higher-order model-checking
  • linear logic
  • relational semantics
  • parity games
  • parametric comonads.

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007. Google Scholar
  2. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics in multiplicative-additive linear logic. Ann. Pure Appl. Logic, 102(3):247-282, 2000. Google Scholar
  3. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Logic, 109(3):205-241, 2001. Google Scholar
  4. M. Coppo, M. Dezani-Ciancaglini, F. Honsell, and G. Longo. Extended Type Structures and Filter Lambda Models. In Logic Colloquium 82, 1984. Google Scholar
  5. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. Google Scholar
  6. Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci., 424:20-45, 2012. Google Scholar
  7. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. Google Scholar
  8. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. C.U.P., 1989. Google Scholar
  9. Charles Grellois and Paul-André Melliès. Indexed linear logic and higher-order model checking. In Intersection Types and Related Systems 2014, EPTCS 177, 2015. Google Scholar
  10. Charles Grellois and Paul-André Melliès. An infinitary model of linear logic. In Andrew M. Pitts, editor, FoSSaCS, volume 9034 of LNCS, 2015. Google Scholar
  11. Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking, MFCS 2015. Google Scholar
  12. Axel Haddad. Shape-preserving transformations of higher-order recursion schemes. PhD thesis, Université Paris Diderot, 2013. Google Scholar
  13. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In LICS, 2008. Google Scholar
  14. Haruo Hosoya, Jerome Vouillon, and Benjamin C. Pierce. Regular expression types for XML. In Martin Odersky and Philip Wadler, editors, ICFP, 2000. Google Scholar
  15. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR'96 Proceedings, volume 1119 of LNCS, pages 263-277. Springer, 1996. Google Scholar
  16. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Zhong Shao and Benjamin C. Pierce, editors, POPL, 2009. Google Scholar
  17. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, 2009. Google Scholar
  18. Paul-André Melliès. Parametric monads and enriched adjunctions. LOLA 2012. Google Scholar
  19. Paul-André Melliès. Functorial boxes in string diagrams. In Zoltán Ésik, editor, CSL, volume 4207 of Lecture Notes in Computer Science, pages 1-30. Springer, 2006. Google Scholar
  20. Paul-André Melliès. Game semantics in string diagrams. In LICS, 2012. Google Scholar
  21. Paul-André Melliès. The parametric continuation monad. Math. Struct. Comp. Sci., 2014. Google Scholar
  22. Paul-André Melliès and Nicolas Tabareau. Resource modalities in game semantics. In LICS, pages 389-398. IEEE Computer Society, 2007. Google Scholar
  23. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90. IEEE Computer Society, 2006. Google Scholar
  24. Sylvain Salvati and Igor Walukiewicz. Recursive schemes, krivine machines, and collapsible pushdown automata. In RP, 2012. Google Scholar
  25. Sylvain Salvati and Igor Walukiewicz. Evaluation is msol-compatible. In FSTTCS, volume 24 of LIPIcs, 2013. Google Scholar
  26. Sylvain Salvati and Igor Walukiewicz. Using models to model-check recursive schemes. In TLCA, volume 7941 of LNCS, 2013. Google Scholar
  27. Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In RTA, volume 15 of LIPIcs, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact