Finite Developments in the Lambda-Calculus

Jean-Jacques Lévy

    Part 1 Parallel moves. Cube lemma. Equivalence by permutations. [Pdf, Pdf4]
    Part 2 Labeled calculus. Redex families. Finite developments. [Pdf, Pdf4]
    Part 3 Proofs and Exercises. [Pdf, Pdf4]

    1. Abramsky, S.; The Lazy Lambda Calculus, Imperial College, 1987.
    2. Amadio, R.; Curien, P.-L.; Domains and Lambda-calculi. Cambridge University Press, 1998.
    3. Barendregt, Henk; The Lambda Calculus. Its Syntax and Semantics, Elsevier, 2nd edition, 1997.
    4. Barendregt, Henk; Lambda calculi with types, Handbook of logic in comp. science, Oxford, 1991.
    5. Berry, G.; Lévy, J.-J.; Minimal and Optimal Computations of Recursive Programs, JACM, 1979.
    6. Church, Alonzo, The calculi of Lambda-Conversion, 1941.
    7. Curry, H.; Feys, R.; Combinatory Logic, Vol. 1. Amsterdam, Netherlands: North-Holland, 1958.
    8. Curry, H.; Hindley R.; Seldin J.; Combinatory Logic, Vol. 2, Universiteit van Amsterdam, Amsterdam, 1972.
    9. Damas L.; Milner R.; Principal type-schemes for functional programs. POPL, 1982.
    10. Girard, J.-Y.; Lafont, Y.; Taylor, P.; Proofs and Types. Cambridge University Press, 1989.
    11. Gonthier, G.; Abadi, M.; Lévy, J.-J.; The Geometry of Optimal Lambda Reduction, POPL'92, Albuquerque, 1992.
    12. Huet, G.; Lévy, J.-J.; Computations in Orthogonal Rewriting Systems, I, Essays in Honor of Alan Robinson, MIT Press, 1991
    13. Huet, G.; Lévy, J.-J.; Computations in Orthogonal Rewriting Systems, II, Essays in Honor of Alan Robinson, MIT Press, 1991
    14. Krivine, Jean-Louis; Lambda-calcul; types et modèles. Masson, 1997.
    15. Lévy, J.-J.; An algebraic interpretation of the lambda-beta-K-calculus; and an application of a labelled lambda-calculus
      Rome Symposium on the Lambda calculus, 1975; also in TCS 2 (1976).
    16. Lévy, J.-J.; Réductions correctes et optimales dans le lambda calcul, Thèse Paris 7, 1978.
    17. Lévy, J.-J.; Optimal reductions in the lambda-calculus, To H.B.Curry: Essays on Combinatory Logic,
      Lambda Calculus and Formalism, Academic Press, 1980.
    18. Ong, Luke; Lambda Calculus, Cours Oxford, 1998.
    19. Peyton Jones, Simon; Lester, David; Implementing functional languages: a tutorial. Prentice Hall, 1992.
    20. Pierce, B. C.; Foundational Calculi for Programming Languages, Handbook of Comp. Sc. and Engineering, 1995.
    21. Pierce, B. C.; Types and Programming Languages, The MIT Press, 2002.
    22. Plotkin, G.; Call-by-name, call-by-value, and the lambda-calculus. Theoretical Computer Science, vol 1, 1975.
    23. van Raamsdonk, F.; Severi, P.; Sorensen, M H B.; B. Hongwei Xi; Perpetual Reductions in lambda-calculus.
      Information and Computation 1999.
    24. Scott, D.; Continuous Lattices, Oxford, PRG-7, 1971.
    25. Scott, D.; Data Type as Lattices, Lecture notes, Amsterdam 1972. Oxford PRG-5, Siam J. on Comp., Sep. 1976.

Lectures at ISR 2021
12th International School on Rewriting, Madrid, 5-16 July 2021