[Prev][Next][Index][Thread]
Paper on (CBV) lambda-mu-calculus
I'd like to announce that the expanded version of my paper presented
at MFCS this summer is now available.
Title: A computational interpretation of the $\lambda\mu$-calculus
WWW: http://www.cl.cam.ac.uk/users/gmb/Publications/cilmu.ps.gz
Abstract:
This paper proposes a simple computational interpretation of
Parigot's $\lambda\mu$-calculus. The $\lambda\mu$-calculus is an
extension of the typed $\lambda$-calculus which corresponds via
the Curry-Howard correspondence to classical logic. Whereas other work
has given computational interpretations by translating the
$\lambda\mu$-calculus into other calculi, I wish to propose here that
the $\lambda\mu$-calculus itself has a simple computational
interpretation: it is a typed $\lambda$-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.
Bibtex:
@TechReport{bierman98:lmutr,
author="G.M.~Bierman",
title="A Computational Interpretation of the $\lambda\mu$-calculus",
institution="University of Cambridge Computer Laboratory",
number=448,
month=sep,
year=1998
}
The MFCS conference version is also available at:
http://www.cl.cam.ac.uk/users/gmb/Publications/mfcs.ps.gz
Bibtex:
@inproceedings{bierman98:mfcs,
author="G.M.~Bierman",
title="A Computational Interpretation of the $\lambda\mu$-calculus",
booktitle="Proceedings of Symposium on Mathematical Foundations of Computer
Science",
series=LNCS,
volume=1450,
pages="336--345",
editor="L.~Brim and J.~Gruska and J.~Zlatu{\u{s}}ka",
month=aug,
year=1998
}