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