| 1 |
01/16 |
Introduction / Dependent Type Theory (Chapters 1 & 2 of the tutorial) |
|
| 2 |
01/23 |
Dependent Type Theory / Propositions and Proofs (Chapters 2 & 3 of the tutorial) |
lean-mode |
| 3 |
01/30 |
Propositions and Proofs / Quantifiers and Equality (Chapters 3 & 4 of the tutorial) |
|
| 4 |
02/06 |
Quantifiers and Equality / Interacting with Lean (Chapter 4 & 5 of the tutorial) |
|
| 5 |
02/13 |
Inductive Types (Chapter 6 of the tutorial) |
Inductive Families |
| 6 |
02/20 |
The formal proof of the Kepler conjecture, Thomas Hales Professor, University of Pittsburgh |
|
| 7 |
02/27 |
Inductive Types, Induction and Recursion (Chapters 6 and 7 of the tutorial) |
|
|
03/06 |
No Class |
Mid-Semester Break |
|
03/13 |
No Class |
Spring Break |
| 8 |
03/20 |
Elaboration and Unification (Leonardo de Moura; Chapter 8 of the tutorial) |
|
| 9 |
03/27 |
Type Classes and Structures (Chapters 9 and 10 of the tutorial) |
Elaboration |
| 10 |
04/03 |
Tactics (Chapter 11 of the tutorial) |
|
| 11 |
04/10 |
Homotopy Type Theory (the-Hott-Book) |
|
| 12 |
04/17 |
Axioms (Chapter 12 of the tutorial) |
Spring Carnival |
| 13 |
04/24 |
Formal Methods in Mathematics |
|
|
05/01 |
No class |
|
