A Term Calculus for Intuitionistic Linear Logic

In this paper we consider the problem of deriving a term assignment system for Girard’s Intuitionistic Linear Logic for both the sequent calculus and natural deduction proof systems. Our system diers from previous calculi (e.g. that of Abramsky [1]) and has two important properties which they lack. These are the substitution property (the set of valid deductions is closed under substitution) and subject reduction (reduction on terms is well-typed). We also consider term reduction arising from cut-elimination in the sequent calculus and normalisation in natural deduction. We explore the relationship between these and consider their computational content.