Lecture outline :
- girard's paradox with one type of all types ;
- difference with Russell's paradox ;
- universe as reflection principle ;
- algebraic proof of canonicity with the Artin gluing technique and normalization proof ;
- application to proof verification.
