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 a direct computational interpretation. This interpretation is best given as a single-step semantics which, in particular, leads to a relatively simple, but powerful, operational theory.
Preview
Unable to display preview. Download preview PDF.
References
G.M. Bierman. A classical linear λ-calculus. Technical Report 401, Cambridge Computer Laboratory 1996.
M. Felleisen. The theory and practice of first-class prompts. POPL 1988.
A.D. Gordon. Bisimilarity as a theory of functional programming: Mini-course. Technical Report NS-95-2, BRICS, Department of Computer Science, University of århus, July 1995.
T.G. Griffin. A formulae-as-types notion of control. POPL 1990.
C.A. Gunter, D. Rémy, and J.G. Riecke. A generalisation of exceptions and control in ML-like languages. FPCA 1995.
R. Harper and C. Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, School of Computer Science, Carnegie Mellon University, June 1997.
M. Hofmann and T. Streicher. Continuation models are universal for λΜ-calculus. LICS 1997.
C.-H.L. Ong and C.A. Stewart. A Curry-Howard foundation for functional computation with control. POPL 1997.
M. Parigot. λΜ-calculus: an algorithmic interpretation of classical natural deduction. LPAR 1992. LNCS 624.
A.M. Pitts. Operational semantics for program equivalence. Slides from talk given at MFPS, 1997.
A.M. Pitts. Operationally-based theories of program equivalence. In Semantics and Logics of Computation, CUP, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bierman, G.M. (1998). A computational interpretation of the λΜ-calculus. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055783
Download citation
DOI: https://doi.org/10.1007/BFb0055783
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive