An Infinitary Model of Linear Logic

DOI10.1007/978-3-662-46678-0_3MaRDI QIDQ2948550zbMATH OpenOpenAlexFDO

Authors Charles Grellois, Paul-André Melliès

Publication date 1 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1411.4380

zbMATH Keywords

linear logicrelational semanticsfixpoint operatorsparity conditionsinduction and coinductionhigher-order model-checking

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Specification and verification (program logics, model checking, etc.) (68Q60)

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 sketching the connection between the resulting model of lambda-calculus with recursion and higher-order model-checking.

Recommendations

• scientific article; zbMATH DE number 29724
• scientific article; zbMATH DE number 1163986
• Models of linear logic
• A modal view of linear logic
• scientific article; zbMATH DE number 17706
• Axioms and models of linear logic
• The finite model property for various fragments of linear logic
• scientific article; zbMATH DE number 1302492
• Infinitary hybrid logic and the Lindelöf property
• Models of transfinite provability logic

Cited in

(8)

• A functorial bridge between the infinitary affine lambda-calculus and linear logic
• Domains for Higher-Order Games
• Generalized bounded linear logic and its categorical semantics
• Finitary semantics of linear logic and higher-order model-checking
• Infinitary lambda calculi from a linear perspective
• A non-uniform finitary relational semantics of system T
• scientific article; zbMATH DE number 29724 (Why is no real title available?)
• Combining fixpoint and differentiation theory

This page was built for publication: An Infinitary Model of Linear Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2948550)