# 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.

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}
}