Around classical and intuitionistic linear logics

DOI10.1145/3209108.3209132MaRDI QIDQ5145339zbMATH OpenOpenAlexWikidataFDO

Authors Olivier Laurent

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209132

zbMATH Keywords

conservativitydouble negationfocusingintuitionistic linear logiclinear logicnegative translationstensor logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) 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)

Recommendations

• Natural deduction for intuitionistic linear logic
• Intuitionistic phase semantics is almost classical
• Functional interpretations of intuitionistic linear logic
• Functional Interpretations of Intuitionistic Linear Logic
• The finite model property for various fragments of intuitionistic linear logic

Cited in

(17)

• Linearizing intuitionistic implication
• Statistics of intuitionistic versus classical logics
• Classical multiplicative linear logic intuitionistic MLL
• On linear Brouwerian logics
• Classical and intuitionistic subexponential logics are equally expressive
• scientific article; zbMATH DE number 1341468 (Why is no real title available?)
• Towards CERes in intuitionistic logic
• Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic
• The ILLTP library for intuitionistic linear logic
• Circular proofs as session-typed processes: a local validity condition
• scientific article; zbMATH DE number 7166981 (Why is no real title available?)
• Intuitionistic phase semantics is almost classical
• Formal Methods in Software and Systems Modeling
• Explorations in Subexponential Non-associative Non-commutative Linear Logic
• Comparing session type systems derived from linear logic
• Around classical and intuitionistic linear processes
• YALLA: yet another deep embedding of linear logic in Rocq

This page was built for publication: Around classical and intuitionistic linear logics

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