Skip to main content
SpringerLink
Log in

Explicit substitutions with de bruijn's levels

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1995)

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

Included in the following conference series:

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

Access this chapter

Log in via an institution

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.

    Google Scholar 

  2. L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2-3):173–202, October 1989.

    Article  Google Scholar 

  3. Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λυ, a calculus of explicit substitutions which preserves strong normalisation. Submitted, December 1994.

    Google Scholar 

  4. P. Crégut. An abstract machine for the normalization of λ-calculus. In Proc. Conf. on Lisp and Functional Programming, pages 333–340. ACM, 1990.

    Google Scholar 

  5. P. Crégut. Machines à environnement pour la réduction symbolique et l'évaluation partielle. PhD thesis, Universite de PARIS 07, 1991.

    Google Scholar 

  6. P.-L. Curien, Th. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. RR 1617, INRIA, Rocquencourt, February 1992.

    Google Scholar 

  7. H. B. Curry, R. Feys, and W. Craig. Combinatory Logic, volume 1. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1958.

    Google Scholar 

  8. N. G. de Bruijn. Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. Koninkl. Nederl. Akademie van Wetenschappen, 75(5):381–392, 1972.

    Google Scholar 

  9. N. G. de Bruijn. Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings. Proc. of the Koninklijke Nederlan Akademie, 81(3):1–9, September 1978. Dedicated to A. Heyting at the occasion his 80th Birrthday on May 9, 1978.

    Google Scholar 

  10. N. G. de Bruijn. A namefree lambda calculus with facilities for internal definition of expressions and segments. TH-Report 78-WSK-03, Technological University Eindhoven, Netherlands, Department of Mathematics, 1978.

    Google Scholar 

  11. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 244–320. Elseviere Science Publishers B. V. (North-Holland), 1990.

    Google Scholar 

  12. J. Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proceedings of the 17th Annual ACM Symposium on Principles Of Programming Languages, Orlando (Fla., USA), pages 1–15, San Fransisco, 1990. ACM.

    Google Scholar 

  13. J. Field. Incremental Reduction in the Lambda Calculus and Related Reduction Systems. PhD thesis, Cornell U., November 1991.

    Google Scholar 

  14. Th. Hardin. Confluence results for the pure strong categorical combinatory logic CCL: λ-calculi as subsystems of CCL. Theoretical Computer Science, 65:291–342, 1989.

    Article  Google Scholar 

  15. M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems. Journal of IPS Japan, 31(5):633–642, 1990.

    Google Scholar 

  16. P. Lescanne. From λσ to λυ, a journey through calculi of explicit substitutions. In Hans Boehm, editor, Proceedings of the 21st Annual ACM Symposium on Principles Of Programming Languages, Portland (Or., USA), pages 60–69. ACM, 1994.

    Google Scholar 

  17. P. Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions λυ. Technical Report RR-2222, INRIA-Lorraine, January 1994.

    Google Scholar 

  18. P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In M. Dezani, editor, Int. Conf. on Typed Lambda Calculus and Applications, 1995.

    Google Scholar 

  19. A. Ríos. Contributions à l'étude des λ-calculs avec des substitutions explicites. Thèse de Doctorat d'Université, U. Paris VII, 1993.

    Google Scholar 

  20. T. Strahm. Partial applicative theories and explicit substitutions. Technical Report IAM 93-008, Univerität Bern, Institut für Informatik und angewandte Mathematik, June 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre de Recherche en Informatique de Nancy (CNRS) and INRIA-Lorraine Campus Scientifique, BP 239, F54506, Vandœuvre-lès-Nancy, France

    Pierre Lescanne & Jocelyne Rouyer-Degli

Authors
  1. Pierre Lescanne
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jocelyne Rouyer-Degli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jieh Hsiang

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lescanne, P., Rouyer-Degli, J. (1995). Explicit substitutions with de bruijn's levels. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_65

Download citation

  • DOI: https://doi.org/10.1007/3-540-59200-8_65

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59200-6

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation