Natural deduction for intuitionistic non-commutative linear logic
| Author(s) : | Frank Pfenning Jeff Polakow, |
| Publisher : | N/A |
| Publication Date : | 1999 |
| ISSN : | N/A |
| Abstract : | Abstract. We present a system of natural deduction and associated term calculus for intuitionistic non-commutative linear logic (INCLL) as a conservative extension of intuitionistic linear logic. We prove subject reduction and the existence of canonical forms in the implicational fragment. 1, |