Technical reports
Strong normalisation for the linear term calculus
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} }