Department of Computer Science and Technology

Technical reports

A computational interpretation of the λμ calculus

G.M. Bierman

September 1998, 10 pages

DOI: 10.48456/tr-448

Abstract

This paper proposes a simple computational interpretation of Parigot’s λμ-calculus. The λμ-calculus is an extension of the typed λ-calculus which corresponds via the Curry-Howard correspondence to classical logic. Whereas other work has given computational interpretations by translating the λμ-calculus into other calculi, I wish to propose here that the λμ-calculus itself has a simple computational interpretation: it is a typed λ-calculus which is able to save and restore the runtime environment. This interpretation is best given as a single-step semantics which, in particular, leads to a relatively simple, but powerful, operational theory.

Full text

PDF (1.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-448,
  author =	 {Bierman, G.M.},
  title = 	 {{A computational interpretation of the $\lambda\mu$
         	   calculus}},
  year = 	 1998,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-448.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-448},
  number = 	 {UCAM-CL-TR-448}
}