Abstract
We present a translation of Parigot's λμ-calculus [10] into the usual λ-calculus. This translation, which is based on the so-called continuation passing style, is correct with respect to equality and with respect to evaluation. At the type level, it induces a logical interpretation of classical logic into intuitionistic one, akin to Kolmogorov's negative translation. As a by-product, we get the normalization of second order typed λμ-calculus.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. W. Appel. Compiling with continuations. Cambridge University Press, 1992.
F. Barbanera and S. Berardi. Continuations and simple types: a strong normalization result. In Proceedings of the ACM SIGPLAN Workshop on Continuations. Report STAN-CS-92-1426, Stanford University, 1992.
F. Barbanera and S. Berardi. Extracting constructive content from classical logic via control-like reductions. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on on Typed Lambda Calculi and Applications, pages 45–59. Lecture Notes in Computer Science, 664, Springer Verlag, 1993.
H.P. Barendregt. The lambda calculus, its syntax and semantics. North-Holland, revised edition, 1984.
J.-Y. Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.
T. G. Griffin. A formulae-as-types notion of control. In Conference record of the seventeenth annual ACM symposium on Principles of Programming Languages, pages 47–58, 1990.
J.-L. Krivine. Lambda-calcul, types et modèles. Masson, 1990.
C. R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the sixth annual IEEE symposium on logic in computer science, pages 96–107, 1991.
C. R. Murthy. A computational analysis of Girard's translation and LC. In Proceedings of the seventh annual IEEE symposium on logic in computer science, pages 90–101, 1992.
M. Parigot. λμ-Calculus: an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 190–201. Lecture Notes in Artificial Intelligence, 624, Springer Verlag, 1992.
M. Parigot. Classical proofs as programs. In G. Gottlod, A. Leitsch, and D. Mundici, editors, Proceedings of the third Kurt Gödel colloquium — KGC'93, pages 263–276. Lecture Notes in Computer Science, 713, Springer Verlag, 1993.
M. Parigot. Strong normalization for second order classical natural deduction. In Proceedings of the eighth annual IEEE symposium on logic in computer science, pages 39–46, 1993.
G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theretical Computer Science, 1:125–159, 1975.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Groote, P. (1994). A CPS-translation of the λμ-calculus. In: Tison, S. (eds) Trees in Algebra and Programming — CAAP'94. CAAP 1994. Lecture Notes in Computer Science, vol 787. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0017475
Download citation
DOI: https://doi.org/10.1007/BFb0017475
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57879-6
Online ISBN: 978-3-540-48373-1
eBook Packages: Springer Book Archive