Abstract
Under the extension of Curry-Howard’s correspondence to classical logic, Gentzen’s NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot’s λμ-calculus and Curien-Herbelin’s \(\bar\lambda\mu\tilde\mu\)-calculus. We aim at showing their computational equivalence. We define translations between these calculi. We prove simulation theorems for an undirected evaluation as well as for call-by-name and call-by-value evaluations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Curien, P.-L., Herbelin, H.: The Duality of Computation. In: Proceedings of the International Conference on Functional Programming (2000)
Dougherty, D.J., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in a language with control operators. In: Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 155–166 (2004)
Gentzen, G.: Investigations into Logical Deduction. In: Szabo, M. (ed.) Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam (1934)
Griffin, T.G.: The Formulae-as-Types Notion of Control. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pp. 47–57. ACM Press, New York (1990)
Ong, L., Stewart, C.: A Curry-Howard foundation for functional computation with control. In: Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages, pp. 215–227. ACM Press, New York (1997)
Parigot, M.: λμ-calculus: an Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rocheteau, J. (2005). λμ-Calculus and Duality: Call-by-Name and Call-by-Value. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)