| Date | Inst | Topics Covered | Attendance | HWs |
|---|---|---|---|---|
| Jan 15 | Vijay, Charles, Chris, and Jeanne | Lec 0: Why learn about type theory? | ||
| Jan 22 | Vijay | Lec 1: Typechecking: How PL theorists specify and implement their type systems |
writeup code solution |
|
| Jan 29 | Jeanne | Lec 2: The Curry-Howard Correspondence: How types and logic are the same. (slides) |
writeup code |
|
| Feb 5 | Jeanne | Lec 3: Phantom Types: A spooky way to get more guarantees from your compiler. (slides) | ||
| Feb 12 | Vijay | Lec 4: Lambda Calculus and Definability: The ability to abstract really gives you all the power you need. (slides) |
writeup code |
|
| Feb 19 | Charles | Lec 5: Subtyping: When some types are greater than others. (slides) | optional | |
| Feb 26 | Jeanne | Lec 6: Generalized Algebraic Datatypes: When normal constructors aren't enough. (slides) | writeup | |
| Mar 5 | Jacob | Guest Lecture 1: Hoare Calculus (slides) | ||
| Mar 12 | Spring Break! No class. | |||
| Mar 19 | Cameron | Guest Lecture 2: Verification | ||
| Mar 26 | Vijay | Lec 7: Compilation: Making code look worse to humans but better to processors (slides) |
writeup code |
|
| Apr 2 | Charles | Lec 8: Typed Assembly: Why not have types everywhere? (slides) | ||
| Apr 9 | Chris | Lec 9: Dependent types: Mixing values with types (lecture notes) |
homework | |
| Apr 16 | Charles | Lec 10: Pure Type Systems: Who needs values anyway? (slides) | homework | |
| Apr 23 | Chris | Lec 11: "Practical" Category Theory: Where are EndoFunctors? Why are Monads Monoids there? | ||
| Apr 30 | Chris | Lec 12: Homotopy Type Theory: The HoTTest type theory. |