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