Lecture outline:
- Russell's 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 verification as type verification.
