Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Relational semantics of linear logic and higher-order model-checking
(Submitted on 20 Jan 2015 (v1), last revised 1 May 2015 (this version, v3))
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 his 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.
Submission history
From: Charles Grellois [view email][v1] Tue, 20 Jan 2015 12:51:34 GMT (124kb,D)
[v2] Wed, 15 Apr 2015 14:35:28 GMT (113kb,D)
[v3] Fri, 1 May 2015 10:11:26 GMT (113kb,D)
Link back to: arXiv, form interface, contact.