Il s'agit de décrire les grandes lignes de la théorie mathématique du lambda-calcul.

Plan initial:

I. Lambda-termes, alpha et beta conversion.
II. Confluence.
III. Eta conversion.
IV. Booléens, entiers de Church, points fixes.
V. Résidus, réduction parallèle.
VI. Arbres de Böhm.
VII. Lambda-calcul simplement typé, normalisation forte.
VIII. Introduction aux types dépendants.
 

Contrôle des connaissances:  exercices hebdomadaires + mini-projet.