Lecture outline :
- russell type theory ;
- church's λ-calculus notation for functions ;
- simple type theory and the HOL system ;
- introduction to dependent types, AUTOMATH system ;
- uniform treatment of mathematical objects and proofs ;
- proof checking as type checking.
