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