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]

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