Plan du cours :
- paradoxe de Girard avec un type de tous les types ;
- différence avec le paradoxe de Russell ;
- univers comme principe de réflexion ;
- preuve algébrique de canonicité avec la technique du collage à la Artin et preuve de normalisation ;
- application à la vérification des preuves.