The relational model is injective for multiplicative exponential linear logic (without weakenings)
DOI10.1016/j.apal.2012.01.004zbMath1251.03080WikidataQ114209365 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
injectivity; relational semantics; linear logic; denotational semantics; full abstraction; relational model; MELL proof-nets
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
03F05: Cut-elimination and normal-form theorems
03F07: Structure of proofs
03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F52: Proof-theoretic aspects of linear logic and other substructural logics
03F03: Proof theory in general (including proof-theoretic semantics)
03B40: Combinatory logic and lambda calculus
Related Items
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
