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