The relational model is injective for multiplicative exponential linear logic (without weakenings)

DOI10.1016/j.apal.2012.01.004zbMath1251.03080OpenAlexW1623703906WikidataQ114209365 ScholiaQ114209365MaRDI QIDQ435194

Daniel de Carvalho, Lorenzo Tortora de Falco

Publication date: 11 July 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2012.01.004

zbMATH Keywords

injectivityrelational semanticslinear logicdenotational semanticsfull abstractionrelational modelMELL proof-nets

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items

A semantic account of strong normalization in linear logic ⋮ Proof Nets, Coends and the Yoneda Isomorphism ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An abstract approach to stratification in linear logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantic measure of the execution time in linear logic
• Linear logic
• Differential interaction nets
• Weak typed Böhm theorem on IMLL
• Head linear reduction and pure proof net extraction
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Syntax vs. semantics: A polarized approach
• Locus Solum: From the rules of logic to the logic of rules
• λμ-calculus and Böhm's theorem
• λ-definable functionals andβη conversion
• Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
• Linear logic and polynomial time
• Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic
• The Separation Theorem for Differential Interaction Nets
• A semantic characterisation of the correctness of a proof net
• Execution time of λ-terms via denotational semantics and intersection types
• Obsessional experiments for linear logic proof-nets
• The Typed Böhm Theorem