Department of Computer Science and Technology

Technical reports

Strong normalisation for the linear term calculus

P.N. Benton

July 1993, 13 pages

DOI: 10.48456/tr-305

Abstract

We provide a strong normalisation result for the linear term calculus which was introduced in (Benton et al. 1992). Rather than prove the result from first principles, we give a translation of linear terms into terms in the second order polymorphic lambda calculus (λ2) which allows the result to be proved by appealing to the well known strong normalisation property of λ2. An interesting feature of the translation is that it makes use of the λ2 coding of a coinductive datatype as the translation of the !-types (exponentials) of the linear calculus.

Full text

PDF (0.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-305,
  author =	 {Benton, P.N.},
  title = 	 {{Strong normalisation for the linear term calculus}},
  year = 	 1993,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-305.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-305},
  number = 	 {UCAM-CL-TR-305}
}