Skip to main content
SpringerLink
Log in

A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8312))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  2. Accattoli, B., Kesner, D.: The structural λ-calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: POPL (1995)

    Google Scholar 

  4. Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge University Press (1998)

    Google Scholar 

  5. Balabonski, T.: A unified approach to fully lazy sharing. In: POPL (2012)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. 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)

    Article  MathSciNet  MATH  Google Scholar 

  8. David, R., Guillaume, B.: A λ-calculus with explicit weakening and explicit substitution. MSCS 11(1), 169–206 (2001)

    MathSciNet  MATH  Google Scholar 

  9. Cosmo, R.D., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. In: MSCS (2003)

    Google Scholar 

  10. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press (1989)

    Google Scholar 

  11. Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: RTA, pp. 135–150 (2010)

    Google Scholar 

  12. Gundersen, T., Heijltjes, W., Parigot, M.: Atomic lambda-calculus: a typed lambda-calculus with explicit sharing. In: LICS (2013)

    Google Scholar 

  13. Gundersen, T., Heijltjes, W., Parigot, M.: Un lambda-calcul atomique. Journées Francophones des Langages Applicatifs (2013)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. Kesner, D., Lengrand, S.: Resource operators for lambda-calculus. Information and Computation 205(4), 419–473 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  16. Krivine, J.-L.: Lambda-calculus types and models. Ellis Horwood, Chichester, UK (1993)

    Google Scholar 

  17. Lamping, J.: An algorithm for optimal lambda calculus reduction. In: POPL, pp. 16–30 (1990)

    Google Scholar 

  18. Lescanne, P.: From lambda-sigma to lambda-upsilon, a journey through calculi of explicit substitutions. In: POPL (1994)

    Google Scholar 

  19. 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)

    Google Scholar 

  20. Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32(2), 198–212 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  21. 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)

    Google Scholar 

  22. Wadsworth, C.P.: Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, University of Oxford (1971)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire Preuves, Programmes, Systèmes CNRS & Université Paris Diderot, France

    Tom Gundersen & Michel Parigot

  2. University of Bath, UK

    Willem Heijltjes

Authors
  1. Tom Gundersen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Willem Heijltjes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michel Parigot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Ken McMillan

  2. University of Innsbruck, Austria

    Aart Middeldorp

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation