#
A Parigot-style linear $\lambda$-calculus for full intuitionistic linear
logic

##
Valeria de Paiva and Eike Ritter

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.

Keywords:
linear logic, $\lambda\mu$-calculus, Curry-Howard isomorphism

2000 MSC:
03B20

*Theory and Applications of Categories,*
Vol. 17, 2006,
No. 3, pp 30-48.

http://www.tac.mta.ca/tac/volumes/17/3/17-03.dvi

http://www.tac.mta.ca/tac/volumes/17/3/17-03.ps

http://www.tac.mta.ca/tac/volumes/17/3/17-03.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/3/17-03.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/3/17-03.ps

TAC Home