Geodesic
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

Voir la notice de l'article provenant de 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 
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/
@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/}
}
TY  - JOUR
AU  - Valeria de Paiva
AU  - Eike Ritter
TI  - A Parigot-style linear $\lambda$-calculus for full intuitionistic linear 
logic
JO  - Theory and applications of categories
PY  - 2006
SP  - 30
EP  - 48
VL  - 17
UR  - http://geodesic.mathdoc.fr/item/TAC_2006_17_a2/
LA  - en
ID  - TAC_2006_17_a2
ER  - 
%0 Journal Article
%A Valeria de Paiva
%A Eike Ritter
%T A Parigot-style linear $\lambda$-calculus for full intuitionistic linear 
logic
%J Theory and applications of categories
%D 2006
%P 30-48
%V 17
%U http://geodesic.mathdoc.fr/item/TAC_2006_17_a2/
%G en
%F TAC_2006_17_a2