Abstract
The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait’s reducibility method.
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
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)
Accattoli, B., Kesner, D.: The structural λ-calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010)
Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995)
Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge University Press (1998)
Balabonski, T.: A unified approach to fully lazy sharing. In: POPL (2012)
Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001)
Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21(4), 685–693 (1980)
David, R., Guillaume, B.: A λ-calculus with explicit weakening and explicit substitution. MSCS 11(1), 169–206 (2001)
Cosmo, R.D., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. In: MSCS (2003)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press (1989)
Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: RTA, pp. 135–150 (2010)
Gundersen, T., Heijltjes, W., Parigot, M.: Atomic lambda-calculus: a typed lambda-calculus with explicit sharing. In: LICS (2013)
Gundersen, T., Heijltjes, W., Parigot, M.: Un lambda-calcul atomique. Journées Francophones des Langages Applicatifs (2013)
Hughes, R.J.M.: Super-combinators: a new implementation method for applicative languages. In: ACM Symposium on Lisp and Functional Programming, pp. 1–10 (1982)
Kesner, D., Lengrand, S.: Resource operators for lambda-calculus. Information and Computation 205(4), 419–473 (2007)
Krivine, J.-L.: Lambda-calculus types and models. Ellis Horwood, Chichester, UK (1993)
Lamping, J.: An algorithm for optimal lambda calculus reduction. In: POPL, pp. 16–30 (1990)
Lescanne, P.: From lambda-sigma to lambda-upsilon, a journey through calculi of explicit substitutions. In: POPL (1994)
Pottinger, G.: A type assignment for the strongly normalizable λ-terms. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561–577. Academic Press, London (1980)
Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32(2), 198–212 (1967)
van Oostrom, V., van de Looij, K.-J., Zwitserlood, M.: Lambdascope: another optimal implementation of the lambda-calculus. In: Workshop on Algebra and Logic on Programming Systems (2004)
Wadsworth, C.P.: Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, University of Oxford (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gundersen, T., Heijltjes, W., Parigot, M. (2013). A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)