Paper Info
Title
An Infinitary Model of Linear Logic.
Abstract
In this paper, we construct an infinitary variant of the relational model of linear logic, where the exponential modality is interpreted as the set of finite or countable multisets. We explain how to interpret in this model the fixpoint operator Y as a Conway operator alternatively defined in an inductive or a coinductive way. We then extend the relational semantics with a notion of color or priority in the sense of parity games. This extension enables us to define a new fixpoint operator Y combining both inductive and coinductive policies. We conclude the paper by mentionning a connection between the resulting model of A-calculus with recursion and higher-order model-checking.
Year
DOI
Venue
2014
10.1007/978-3-662-46678-0_3
Lecture Notes in Computer Science
Keywords
DocType
Volume
Linear logic,relational semantics,fixpoint operators,induction and coinduction,parity conditions,higher-order model-checking
Journal
9034
ISSN
Citations 
PageRank 
0302-9743
3
0.42
References 
Authors
13
2
Name
Order
Citations
PageRank
Charles Grellois1112.64
Paul-andré Melliès239230.70