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

DOI10.1016/J.APAL.2012.01.004MaRDI QIDQ435194zbMATH OpenOpenAlexWikidataFDO

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

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)

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

Cites work

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

Cited in

(9)

• Obsessional experiments for linear logic proof-nets
• scientific article; zbMATH DE number 7566060 (Why is no real title available?)
• An abstract approach to stratification in linear logic
• A semantic account of strong normalization in linear logic
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• 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
• Causality in linear logic. Full completeness and injectivity (unit-free multiplicative-additive fragment)

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)