Technical reports
A classical linear λ-calculus
Gavin Bierman
July 1996, 41 pages
DOI: 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} }