Skip to main content
SpringerLink
Log in

Characterising Strong Normalisation for Explicit Substitutions

  • Conference paper
  • First Online:
LATIN 2002: Theoretical Informatics (LATIN 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2286))

Included in the following conference series:

Abstract

We characterise the strongly normalising terms of a composition-free calculus of explicit substitutions (with or without garbage collection) by means of an intersection type assignment system. The main novelty is a cut-rule which allows to forget the context of the minor premise when the context of the main premise does not have an assumption for the cut variable.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

    Article  MathSciNet  Google Scholar 

  2. R. M. Amadio and P.-L. Curien. Domains and lambda-calculi. Cambridge University Press, Cambridge, 1998.

    Book  Google Scholar 

  3. S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102(1):135–163, 1992.

    Article  MathSciNet  Google Scholar 

  4. S. van Bakel. Intersection Type Assingment Systems. Theoretical Computer Science, 151(2):385–435, 1995.

    Article  MathSciNet  Google Scholar 

  5. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931–940, 1983.

    Article  MathSciNet  Google Scholar 

  6. Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λv, a calculus of explicit substitutions which preserves strong normalization. Journal of Functional Programming, 6(5):699–722, 1996.

    Article  MathSciNet  Google Scholar 

  7. R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computer Science in the Netherlands, pages 62–72. Koninklijke Jaarbeurs, 1995.

    Google Scholar 

  8. M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685–693, 1980.

    Article  MathSciNet  Google Scholar 

  9. M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and λ-calculus semantics. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 535–560. Academic Press, London, 1980.

    Google Scholar 

  10. M. Dezani-Ciancaglini, F. Honsell, and Y. Motohama. Compositional characterization of λ-terms using intersection types. In Mathematical Foundations of Computer Science 2000, volume 1893 of Lecture Notes in Computer Science, pages 304–313. Springer, 2000.

    Chapter  Google Scholar 

  11. D. Dougherty and P. Lescanne. Reductions, intersection types and explicit substitutions. In Typed Lambda Calculi and Applications 2001, volume 2044 of Lecture Notes in Computer Science, pages 121–135. Springer, 2001.

    Chapter  Google Scholar 

  12. J. Gallier. Typing untyped λ-terms, or reducibility strikes again! Annals of Pure and Applied Logic, 91:231–270, 1998.

    Article  MathSciNet  Google Scholar 

  13. S. Ghilezan. Strong normalization and typability with intersection types. Notre Dame Journal of Formal Logic, 37(1):44–52, 1996.

    Article  MathSciNet  Google Scholar 

  14. J.-Y. Girard. Une extension de l’interprétation de Gödel á l’analyse, et son application á l’elimination des coupures dans l’analyse et la théorie des types. In 2nd Scandinavian Logic Symposium, pages 63–92. North-Holland, 1971.

    Google Scholar 

  15. F. Kamareddine and A. Rios. Extending a λ-calculus with explicit substitutions which preserves strong normalization into a confluent calculus of open terms. Journal of Functional Programming, 7(4):395–420, 1997.

    Article  MathSciNet  Google Scholar 

  16. J.-L. Krivine. Lambda-calcul Types et modèles. Masson, Paris, 1990.

    MATH  Google Scholar 

  17. D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44(1):51–68, 1986.

    Article  MathSciNet  Google Scholar 

  18. S. Lengrand, D. Dougherty, and P. Lescanne, An improved system of intersection types for explicit substitutions, Internal Report, ENS de Lyon, 2001.

    Google Scholar 

  19. P.-A. Melliès. Typed λ-calculi with explicit substitution may not terminate. In Typed Lambda Calculi and Applications 2001, volume 902 of Lecture Notes in Computer Science, pages 328–334. Springer, 1995.

    Chapter  Google Scholar 

  20. J. C. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, volume B, pages 415–431. Elsevire, Amsterdam, 1990.

    Google Scholar 

  21. J. C. Mitchell. Foundation for Programmimg Languages. MIT Press, 1996.

    Google Scholar 

  22. G. Pottinger. A type assignment for the strongly normalizable λ-terms. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 561–577. Academic Press, London, 1980.

    Google Scholar 

  23. E. Ritter. Characterizing explicit substitutions which preserve termination. In Typed Lambda Calculi and Applications 1999, volume 1581 of Lecture Notes in Computer Science, pages 325–339. Springer, 1999.

    Chapter  Google Scholar 

  24. P. Severi. Normalisation in lambda calculus and its relation to type inference. PhD thesis, Eindhoven University of Technology, 1996.

    Google Scholar 

  25. W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32:198–212, 1967.

    Article  MathSciNet  Google Scholar 

  26. W. W. Tait. A realizability interpretation of the theory of species. In Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 240–251. Springer, 1975.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queen’s Gate, SW7 2BZ, London, UK

    Steffen van Bakel

  2. Dipartimento di Informatica, Universitá di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Mariangiola Dezani-Ciancaglini

Authors
  1. Steffen van Bakel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Compaq Cambridge Research Laboratory, One Cambridge Center, 02142-1612, Cambridge, MA, USA

    Sergio Rajsbaum

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Bakel, S., Dezani-Ciancaglini, M. (2002). Characterising Strong Normalisation for Explicit Substitutions. In: Rajsbaum, S. (eds) LATIN 2002: Theoretical Informatics. LATIN 2002. Lecture Notes in Computer Science, vol 2286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45995-2_33

Download citation

  • DOI: https://doi.org/10.1007/3-540-45995-2_33

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43400-9

  • Online ISBN: 978-3-540-45995-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation