Cours de Lambda-calcul.

I. Cours de 3ème cycle, en français (donné en 2001, 2002, 2003)

(DEA de Logique mathématique et Fondements de l'informatique,
UFR de Mathématiques, Université Paris 7),

Le cours.

Chapitre 0. Une introduction au lambda-calcul,
                   voir "compléments", en bas de la page, 10 p.
Chapitre 1. Syntaxe du lambda-calcul non typé (1)
                  Termes, substitutions, réductions; Théorème de Church-Rosser,
                   version du 30 Janvier 2002, 20 p. (format  postscript)
Chapitre 2. Syntaxe du lambda-calcul non typé (2)
                  Termes résolubles, fnt et stratégies de réduction, normalisation et standardisation.
              version du 5 Février 2002+, 10 p. (format  postscript).
Chapitre 3. Représentation des fonctions récursives.
                    version du 20 Février 2002, 9 p. (format postscript)

Chapitre 4. Le Système E et
                  Les théorèmes de normalisation du lambda-calcul non typé.
                    version du 22 Février 2002, 17 p. (format  postscript )
Chapitre 5. Le Système F  et  le polymorphisme.
                    version du 5 Mars 2002, rev. 2003, 20 p. (format  postscript )
Chapitre AF2. Le Système AF2 et la programmation correcte par preuves.
                   version (provisoire) du 19 Mars 2002, rev. 2003, 20 p. (format postscript )

Chapitre 6. Sémantiques fonctionnelles du lambda-calcul
                   (La sémantique continue et la sémantique stable, applications et limites).
                    version du 29 Mars 2002, rev. 15/03/03, 30 p. (format  postscript )
Chapitre 7. Constructions et comparaisons de modèles du lambda-calcul non typé.
                   (deux méthodes élémentaires de construction : complétions de trame et forcing,
                    et remarques sur les théories équationnelles des modèles)
                   version du 30 Mars 2001+, 22 p. (format  postscript ).

Chapitre 8. Dualité Modèles-Systèmes.
                    version du 30 Avril 2001, 12 p. (format  postscript )

Chapitre SEP. Syntaxe du lambda-calcul non typé (3)
                  Séparabilité forte et Théorème de Böhm.
                  version de 1995, révisée 30 Mars 2001, 6 p. (format postscript ).

Compléments:
-Chapitre 0. Une introduction au lambda-calcul
 (version informelle de 1995, légèrement rafraîchie 2002, 10p.) (format  postscript )
-A presentation of the Curry-Howard correspondence (in english) (format  postscript)
-Simple models of System F, MFPS'14 talk, 15 p., 1998 (in english) (format .ps )

Examens et exercices:
- examen du 12/04/02 ( .ps )
- examen du 22/04/03 ( .ps )
- exercices de programmation "directe" en lambda-calcul  (.ps )
- à compléter.

Lectures  complémentaires éclairantes:
Abbas Edalat, Domain Theory and Exact Computation (en englais), se trouve dans la rubrique "teaching" de sa page web.
(applications de la théorie des domaines à la calculabilité exacte sur les réels et à ses applications, par exemple graphiques).
Eclaire en particulier les notions abstraites sur les domaines introduites dans le Chapitre 6 de mon cours.
- à compléter.

Mes archives.
Chapitre  E.  Théorèmes de normalisation et Système E, version du 13 Juin 1997, 16 p.(format postscript).

II. Tutorial-Survey-Research, in English.

From Computation to Foundations via Functions and Application:
the Lambda-calculus and its Webbed Models,
Theor. Comput. Sci. 249, p.81-161, 2000.

This paper is issued from a conference for algebraists. Its first half is intended for a large audience of mathematicians, and begins as a course on untyped lambda-calculus and its models (in the denotational semantics). Then the paper goes rather deeply in the direction of models, turns into a research paper, and finally surveys the most recent results and open questions in the area. This course is centered on models as such, and not on intersection type asignment systems, as are the notes above. In particular the usual normalisation theorems for untyped lambda-calculus are proved directly using the Engeler-Plotkin model, instead of its dual intersection type system ( which we called System E above) (there is a gain !). The close duality between models and intersection type systems is explained in the paper.