Lambda-calcul
Alonzo Church, The calculi of Lambda-Conversion

Jean-Jacques Lévy ( page à l'X )

    Cours 1 La lambda notation. Lambda-expressions; règles de réduction.
    Cours 2 Redexs et confluence locale. Confluence.
    Cours 3 Récursivité. Développements finis.
    Cours 4 Standardisation. Normalisation. Stratégies de réduction.
    Cours 5 Sémantique cohérente. Approximations d'une expression.
    Cours 6 Arbres de Bohm. Théorème de continuité.
    Cours 7 Domaines de Scott. Modèle D_infini.
    Cours 8 Lambda-calcul typé. Polymorphisme de ML.
    Cours 9 Normalisation forte. Système F.

    Le polycopié [en .Pdf]    Projets [ 1, 2, 3, 4, 5, 6 ]
    Emploi du temps

    Bibliographie

    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. Church, Alonzo, The calculi of Lambda-Conversion, 1941.
    6. Curry, H.; Feys, R.; Combinatory Logic, Vol. 1. Amsterdam, Netherlands: North-Holland, 1958.
    7. Curry, H.; Hindley R.; Seldin J.; Combinatory Logic, Vol. 2, Universiteit van Amsterdam, Amsterdam, 1972.
    8. Damas L.; Milner R.; Principal type-schemes for functional programs. POPL, 1982.
    9. Girard, J.-Y.; Lafont, Y.; Taylor, P.; Proofs and Types. Cambridge University Press, 1989.
    10. Hardin, T.; Cours de Lambda-calcul, DEA-SPP, 1988.
    11. Krivine, Jean-Louis; Lambda-calcul; types et modèles. Masson, 1997.
    12. Lévy, J.-J.; Réductions correctes et optimales dans le lambda calcul, Thèse Paris 7, 1978.
    13. Ong, Luke; Lambda Calculus, Cours Oxford, 1998.
    14. Peyton Jones, Simon; Lester, David; Implementing functional languages: a tutorial. Prentice Hall, 1992.
    15. Pierce, B. C.; Foundational Calculi for Programming Languages, Handbook of Comp. Sc. and Engineering, 1995.
    16. Pierce, B. C.; Types and Programming Languages, The MIT Press, 2002.
    17. Plotkin, G.; Call-by-name, call-by-value, and the lambda-calculus. Theoretical Computer Science, vol 1, 1975.
    18. Scott, D.; Continuous Lattices, Oxford, PRG-7, 1971.
    19. Scott, D.; Data Type as Lattices, Lecture notes, Amsterdam 1972. Oxford PRG-5, Siam J. on Comp., Sep. 1976.
    20. Thompson, Simon; Haskell: The Craft of Functional Programming, Addison-Wesley, 1999.
    21. Weis, Pierre; Leroy, Xavier; Le langage Caml, InterEditions, Paris 1993.

Cours INF 571,
Ecole Polytechnique, 2005-2006