Accueil
Connexion
DENIF –
Documents d’Enseignement Numériques en Informatique Fondamentale
Thèmes
Cursus
Enseignants
Lambda-calcul (Berline)
Thème :
Sémantique
–
Cursus :
LMFI
2003 - 2004
Ce cours a été donné en 2001, 2002, et 2003.
Cours
Chantal Berline
0. Une introduction au lambda-calcul (informelle).
1. Syntaxe du lambda-calcul non typé (1) Termes, substitutions, réductions; Théorème de Church-Rosser.
2. Syntaxe du lambda-calcul non typé (2) Termes résolubles, fnt et stratégies de réduction, normalisation et standardisation.
3. Représentation des fonctions récursives.
4. Le Système E et les théorèmes de normalisation du lambda-calcul non typé.
5. Le Système F et le polymorphisme.
6. Sémantiques fonctionnelles du lambda-calcul.
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).
8. Dualité Modèles-Systèmes.
Bonus. Syntaxe du lambda-calcul non typé (3) Séparabilité forte et Théorème de Böhm.
Complément; A presentation of the Curry-Howard correspondence.
Complément. Simple models of System F.
Complément. Théorèmes de normalisation et Système E.
Examens
Chantal Berline
Examen de 2002
Examen de 2003