Paper Info
Title
Finitary semantics of linear logic and higher-order model-checking.
Abstract
In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the lambda Y-calculus formulated in a companion paper, and to replace it by a finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme G, the finiteness of its interpretation in the resulting model enables us to associate to any MSO formula phi a higher-order recursion scheme G phi resolving the selection problem.
Year
DOI
Venue
2015
10.1007/978-3-662-48057-1_20
Lecture Notes in Computer Science
Keywords
Field
DocType
Higher-order model-checking,Linear logic,Selection problem,Finitary semantics,Parity games
Discrete mathematics,Combinatorics,Model checking,Lattice (order),Kripke semantics,Finitary,Pushdown automaton,Linear logic,Recursion,Mathematics,Lambda
Journal
Volume
ISSN
Citations 
9234
0302-9743
1
PageRank 
References 
Authors
0.35
13
2
Name
Order
Citations
PageRank
Charles Grellois1112.64
Paul-andré Melliès239230.70