Weak typed Böhm theorem on IMLL

DOI10.1016/j.apal.2006.06.001zbMath1110.03056OpenAlexW1615262499MaRDI QIDQ866556

Satoshi Matsuoka

Publication date: 14 February 2007

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.2006.06.001

zbMATH Keywords

linear logicseparationproof netsgraph isomorphisms

Mathematics Subject Classification ID

Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)

Related Items

A coding theoretic study of MLL proof nets, A type-assignment of linear erasure and duplication, The relational model is injective for multiplicative exponential linear logic (without weakenings), Unnamed Item, Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The structure of multiplicatives
• Exhausting strategies, joker games and full completeness for IMLL with unit
• λ-definable functionals andβη conversion
• Completeness, invariance and λ-definability
• Obsessional experiments for linear logic proof-nets
• The Typed Böhm Theorem