Slides
| week | date | topics | slides/homework |
|---|---|---|---|
| 1 | 03.08 | Introduction to Proof Assistants | |
| 2 | 03.15 | HOL Light | |
| 3 | 03.22 | LCF Kernel and Lambda Calc | |
| 4 | 04.12 | More lambda calculus | |
| 5 | 04.19 | Types, STT | |
| 6 | 04.26 | STT Properties | |
| 7 | 05.03 | Lambda-P | |
| 8 | 05.10 | Lambda-2 | |
| 9 | 05.17 | Presentations | |
| 10 | 05.31 | Dependent HOL | |
| 11 | 06.07 | Final Test | homework: auto |
| 12 | 06.14 | ITP Hammers and Automation |