Plan du cours :
- théorie des types de Russell ;
- notation du λ-calcul de Church pour les fonctions ;
- théorie des types simples et système HOL ;
- introduction aux types dépendants, système AUTOMATH ;
- traitement uniforme des objets et des preuves mathématiques ;
- vérification des preuves comme vérification des types.
