Department of Computer Science and Technology

Technical reports

Term assignment for intuitionistic linear logic (preliminary report)

Nick Benton, Gavin Bierman, Valeria de Paiva

August 1992, 57 pages

DOI: 10.48456/tr-262

Abstract

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 differs from previous calculi (e.g. that of Abramsky) 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 define a simple (but more general than previous proposals) categorical model for Intuitionistic Linear Logic and show how this can be used to derive the term assignment system.

We also consider term reduction arising from cut-elimination in the sequent calculus and normalisation in natural deduction. We explore the relationship between these, as well as with the equations which follow from our categorical model.

Full text

PDF (1.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-262,
  author =	 {Benton, Nick and Bierman, Gavin and de Paiva, Valeria},
  title = 	 {{Term assignment for intuitionistic linear logic
         	   (preliminary report)}},
  year = 	 1992,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-262.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-262},
  number = 	 {UCAM-CL-TR-262}
}