The lambda calculus as an abstract data type

  • Pierre Lescanne
Invited Presentations
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λν, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 1996. To appear.Google Scholar
  2. 2.
    N. Bourbaki. Éléments de mathématiques: Théories des ensembles, volume 1. Hermann & Cie, 1954.Google Scholar
  3. 3.
    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
  4. 4.
    H. B. Curry, R. Feys, and W. Craig. Combinatory Logic, volume 1. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1958.Google Scholar
  5. 5.
    N. G. de Bruijn. Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings. Proc. of the Koninklijke Nederlands Akademie, 81(3):1–9, September 1978. Dedicated to A. Heyting at the occasion of his 80th Birthday on May 9, 1978.Google Scholar
  6. 6.
    Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher-order unification via explicit substitutions, extended abstract. In Dexter Kozen, editor, Proceedings 10th IEEE Symposium on Logic in Computer Science, San Diego, California, USA, pages 366–374, June 1995.Google Scholar
  7. 7.
    J. V. Guttag, J. J. Horning, S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.Google Scholar
  8. 8.
    Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors. Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types, WADT11. Oslo Norway, September 1995. Springer LNCS, 1996.Google Scholar
  9. 9.
    D. Hilbert. Die logischen Grundlagen der Mathematik. Mathematische Annalen, 88:151–165, 1923.Google Scholar
  10. 10.
    J. Horning. The Larch Shared Language: Some Open Problems. This volume [8], 1996.Google Scholar
  11. 11.
    A. C. Leisenring. Mathematical logic and Hilbert's ε-symbol. University Mathematical Series, Bedford College, London, 1969.Google Scholar
  12. 12.
    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
  13. 13.
    C. Muñoz. Confluence and preservation of strong normalisation in an explicit substitutions calculus. In Proceedings 11th IEEE Symposium on Logic in Computer Science, Rudgers (New Jersey, USA), 1996. also INRIA Tech-Report 2762.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Pierre Lescanne
    • 1
  1. 1.INRIA-LorraineCentre de Recherche en Informatique de Nancy (CNRS)Vandœuvre-lès-NancyFrance

Personalised recommendations