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