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

DOI10.1016/J.APAL.2012.01.004zbMATH Open1251.03080OpenAlexW1623703906WikidataQ114209365 ScholiaQ114209365MaRDI QIDQ435194FDOQ435194

Authors: 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

Recommendations

• The relational model is injective for multiplicative exponential linear logic
• A semantic account of strong normalization in linear logic
• Relational proof system for linear and other substructural logics
• Obsessional experiments for linear logic proof-nets
• Computing connected proof(-structure)s from their Taylor expansion

zbMATH Keywords

full abstractionlinear logicrelational semanticsdenotational semanticsinjectivityrelational modelMELL proof-nets

Mathematics Subject Classification ID

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

Cites Work

• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Linear logic
• Execution time of λ-terms via denotational semantics and intersection types
• Title not available (Why is that?)
• A semantic measure of the execution time in linear logic
• Differential interaction nets
• Locus solum: From the rules of logic to the logic of rules.
• \(\lambda\mu\)-calculus and Böhm's theorem
• Linear logic and polynomial time
• The Separation Theorem for Differential Interaction Nets
• A semantic characterisation of the correctness of a proof net
• Obsessional experiments for linear logic proof-nets
• Title not available (Why is that?)
• λ-definable functionals andβη conversion
• The Typed Böhm Theorem
• Head linear reduction and pure proof net extraction
• Syntax vs. semantics: A polarized approach
• Observational equivalence and full abstraction in the symmetric interaction combinators
• Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic
• Title not available (Why is that?)
• Weak typed Böhm theorem on IMLL

Cited In (8)

• Title not available (Why is that?)
• An abstract approach to stratification in linear logic
• A semantic account of strong normalization in linear logic
• Title not available (Why is that?)
• Computing connected proof(-structure)s from their Taylor expansion
• The relational model is injective for multiplicative exponential linear logic
• Proof nets, coends and the Yoneda isomorphism
• Obsessional experiments for linear logic proof-nets

This page was built for publication: The relational model is injective for multiplicative exponential linear logic (without weakenings)

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