Natural deduction for intuitionistic linear logic

DOI10.1016/0168-0072(93)E0078-3zbMath0817.03002MaRDI QIDQ1891252

A. S. Troelstra

Publication date: 27 July 1995

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

zbMATH Keywords

natural deductioncategorical modelsstrong normalizationintuitionistic linear logicstrong validitystorage operator

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

New Curry-Howard terms for full linear logic ⋮ Experiments in linear natural deduction ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Three faces of natural deduction ⋮ Natural deduction bottom up ⋮ Full Lambek Calculus in natural deduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Computational interpretations of linear logic
• Constructivism in mathematics. An introduction. Volume II
• Existential instantiation and normalization in sequent natural deduction
• Computer science logic. 6th workshop, CSL '92, San Miniato, Italy, September 28 -- October 2, 1992. Selected papers
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Strong normalisation for the linear term calculus

This page was built for publication: Natural deduction for intuitionistic linear logic