| week | date | topics | slides |
|---|
| 1 | 03.07 | Introduction to Proof Assistants | pdf |
| 2 | 03.14 | LCF, HOL Calculus, HOL kernel | pdf |
| 3 | 03.21 | Lambda Calculus | pdf |
| 4 | 03.28 | Lambda Encoding, Type Checking | pdf |
| 5 | 04.04 | Type Inference, Simple Types | pdf |
| 6 | 04.25 | Exercises only | |
| 7 | 05.02 | Simple Type Theory, Dependent Types | pdf |
| 8 | 05.09 | Lambda P | pdf |
| 9 | 05.16 | Second order propositional logic | pdf |
| 10 | 05.23 | Lambda 2, Paradoxes and Girard | pdf |
| 11 | 05.30 | Set Theory Formally, Code Extraction, Automation | pdf |
| 12 | 06.13 | Presentations 1: Agda,MetaMath,Lean,Cristal |
| 13 | 06.20 | Presentations 2: MLTT, ACL2, seL4, SMTCoq |
| 14 | 07.01 | Final Test, 14:15, SR12 | |