| Date | Inst | Topics Covered | Reading | HWs |
|---|---|---|---|---|
| Jan 16 | Vijay, Charles, Chris, and Jeanne | Lec 1: Types and how we write about them. Notation notation notation. (slides) (sample code) | HW 1 | |
| Jan 23 | Chris | Lec 2: Algebraic Datatypes. Then, Calculus with Datatypes. Then, surprise, calculus actually gives you meaningful types! (lecture notes) | Paper justifying subtraction and division by types |
HW 2 code solution |
| Jan 30 | Chris | Lec 3: Types are actually theorems and programs are actually proofs. (lecture notes) | HW 3 pdf solutions code | |
| Feb 6 | Jeanne | Lec 4: Parsing and ASTs: You need to parse before you can typecheck. Plus, wacky syntax. (notes) | HW 4 pdf solutions code | |
| Feb 13 | Charles | Lec 5: Type Checking: What you're missing out on when you're coding in Python. | HW 5 pdf code | |
| Feb 20 | Vijay | Lec 6: Type Inference: How to do typechecking when no one will tell you what types you're checking. (slides) | HW 6 code solutions | |
| Feb 27 | Midterm | Solutions | ||
| Mar 6 | Charles | Lec 7: Dynamics. How programming languages actually run. Also, you'll understand why we really do need types. | HW 7 code | |
| Mar 20 | Jeanne | Lec 8: Refinement Types. They're types with predicates that make it a lot harder to get your code to typecheck, but also make it a lot easier to ensure your code is correct. (notes) | HW 8 | |
| Mar 27 | Vijay | Lec 9: Lambda Calculus and Definability: learning that the ability to abstract really gives you all the power you need (slides) | HW 9 code | |
| Apr 1 | Charles | Lec ??: Dented Types. We teach something we made up and hope no one notices. ( slides) ( sample code) | HW ?? | |
| Apr 3 | Vijay | Lec 10: Compilation: Making code look worse to humans but better to processors slides | 15-411 | HW 10 code |
| Apr 10 | Chris | Lec 11: "Practical" Category Theory: Where are EndoFunctors? Why are Monads Monoids there? | I stole everything from this guy | HW 11 |
| Apr 17 | Chris | Lec 12: Higher Category Theory: Math is all about drawing squares | No HW. Carnival! | |
| Apr 24 | Charles | Lec 13: Types in the Real World: Charles tries to convince you that you'll use type theory in your real life. slides | HW 13 | |
| May 1 | Final Exam |