| Date | Inst | Topics Covered | Attendance | HWs |
|---|---|---|---|---|
| Aug 28 | Vijay, Charles, Chris, and Jeanne | Lec 0: Why learn about type theory? | ||
| Sep 4 | Vijay | Lec 1: Typechecking: How true PL pros specify and implement their type systems |
writeup code solution |
|
| Sep 11 | Vijay | Lec 2: Lambda Calculus and Definability: The ability to abstract really gives you all the power you need. slides |
writeup code solution |
|
| Sep 18 | Jeanne | Lec 3: The Curry-Howard Correspondence: How types and logic are the same. (slides) |
writeup code |
|
| Sep 25 | Jeanne | Lec 4: Phantom Types: A spooky way to get more guarantees from your compiler. (slides) |
writeup |
|
| Oct 2 | Charles | Lec 5: Subtyping: When some types are greater than others. (slides) | writeup |
|
| Oct 9 | Vijay | Lec 6: Recursion: Recursion, memoization, mutual recursion, and open recursion. notes |
writeup code solution |
|
| Oct 16 | Jeanne | Lec 7: Generalized Algebraic Datatypes: When normal constructors aren't enough. (slides) | writeup | |
| Oct 23 | Charles | Lec 8: Memory: Because garbage collection is not the only way. (slides) | writeup | |
| Oct 30 | Jeanne | Lec 9: Modules: Are functors values? What actually is the type of a structure? (slides) | writeup | |
| Nov 6 | Vijay | Lec 10: Compilation: Making code look worse to humans but better to processors slides |
writeup code solution |
|
| Nov 13 | Chris | Lec 11: Dependent types: Mixing values with types | ||
| Nov 20 | No class! Thanksgiving break. | |||
| Nov 27 | Chris | Lec 12: "Practical" Category Theory: Where are EndoFunctors? Why are Monads Monoids there? |
writeup solution |
|
| Dec 4 | Charles | Lec 13: Pure Type Systems: Who needs values anyway? slides |