Natural deduction for intuitionistic linear logic
From MaRDI portal
Publication:1891252
DOI10.1016/0168-0072(93)E0078-3zbMath0817.03002MaRDI QIDQ1891252
Publication date: 27 July 1995
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
natural deduction; categorical models; strong normalization; intuitionistic linear logic; strong validity; storage operator
03F05: Cut-elimination and normal-form theorems
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
New Curry-Howard terms for full linear logic, Experiments in linear natural deduction, 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