A Parigot-style linear $\lambda$-calculus for full intuitionistic linear
logic
Theory and applications of categories, Chu spaces: theory and applications, Tome 17 (2006), pp. 30-48
Cet article a éte moissonné depuis la source Theory and Applications of Categories website
This paper describes a natural deduction formulation for Full Intuitionistic Linear Logic (FILL), an intriguing variation of multiplicative linear logic, due to Hyland and de Paiva. The system FILL resembles intuitionistic logic, in that all its connectives are independent, but resembles classical logic in that its sequent-calculus formulation has intrinsic multiple conclusions. From the intrinsic multiple conclusions comes the inspiration to modify Parigot's natural deduction systems for classical logic, to produce a natural deduction formulation and a term assignment system for FILL.
Classification :
03B20
Keywords: linear logic, $\lambda\mu$-calculus, Curry-Howard isomorphism
Keywords: linear logic, $\lambda\mu$-calculus, Curry-Howard isomorphism
@article{TAC_2006_17_a2,
author = {Valeria de Paiva and Eike Ritter},
title = {A {Parigot-style} linear $\lambda$-calculus for full intuitionistic linear
logic},
journal = {Theory and applications of categories},
pages = {30--48},
year = {2006},
volume = {17},
language = {en},
url = {http://geodesic.mathdoc.fr/item/TAC_2006_17_a2/}
}
Valeria de Paiva; Eike Ritter. A Parigot-style linear $\lambda$-calculus for full intuitionistic linear logic. Theory and applications of categories, Chu spaces: theory and applications, Tome 17 (2006), pp. 30-48. http://geodesic.mathdoc.fr/item/TAC_2006_17_a2/