Department of Computer Science and Technology

Technical reports

A classical linear λ-calculus

Gavin Bierman

July 1996, 41 pages

DOIhttps://doi.org/10.48456/tr-401

Abstract

This paper proposes and studies a typed λ-calculus for classical linear logic. I shall give an explanation of a multiple-conclusion formulation for classical logic due to Parigot and compare it to more traditional treatments by Prawitz and others. I shall use Parigot’s method to devise a natural deduction fomulation of classical linear logic. This formulation is compared in detail to the sequent calculus formulation. In an appendix I shall also demonstrate a somewhat hidden connection with the paradigm of control operators for functional languages which gives a new computational interpretation of Parigot’s techniques.

Full text

PDF (1.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-401,
  author =	 {Bierman, Gavin},
  title = 	 {{A classical linear $\lambda$-calculus}},
  year = 	 1996,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-401.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-401},
  number = 	 {UCAM-CL-TR-401}
}