Full intuitionistic linear logic

DOI10.1016/0168-0072(93)90146-5zbMath0873.03006OpenAlexW2112970627WikidataQ56994605 ScholiaQ56994605MaRDI QIDQ1314646

J. M. E. Hyland, V. C. V. de Paiva

Publication date: 27 March 1994

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(93)90146-5

zbMATH Keywords

cut eliminationcategorical modelsmultiplicative disjunctionFull Intuitionistic Linear Logicinterpretation of proofsterm assignment system

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

1998 European Summer Meeting of the Association for Symbolic Logic ⋮ Multiple Conclusion Linear Logic: Cut Elimination and More ⋮ Eilenberg-Kelly reloaded ⋮ Coherence via focusing for symmetric skew monoidal categories ⋮ A note on full intuitionistic linear logic ⋮ A comparison between monoidal and substructural logics ⋮ Experiments in linear natural deduction ⋮ Unnamed Item ⋮ Commutative Lambek grammars ⋮ Monoidal logics: completeness and classical systems ⋮ Proof theory in the abstract ⋮ Investigations into a left-structural right-substructural sequent calculus ⋮ On sheaf cohomology and natural expansions ⋮ A FORMALIZATION OF KANT’S TRANSCENDENTAL LOGIC ⋮ Jets and differential linear logic ⋮ Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• *-autonomous categories. With an appendix by Po-Hsiang Chu
• The system \({\mathcal F}\) of variable types, fifteen years later
• A game semantics for linear logic
• Some Syntactical Observations on Linear Logic
• The correspondence between cut-elimination and normalization
• Polycategories
• Normalization as a homomorphic image of cut-elimination
• A dialectica-like model of linear logic
• Proof theory