This is a class about type theory at CMU.
It is taught by Thejaswi Kadur, Jacob Neumann, Cameron Wong, and Ariel Davis.
It was taught in the past by Vijay Ramamurthy, Jeanne VanBriesen, Chris Grossack, and Charles Yuan.
Subject to change. After the lecture, notes/slides will be posted under "What" and homework will be posted under "HW".
| When | Who | What | HW |
|---|---|---|---|
| 27 Aug | Ariel | Type Theory for Programmers | HW01 |
| 03 Sep | Thejas | Algebraic Data Types | HW02 |
| 10 Sep | Thejas | Phantom Types | None |
| 17 Sep | Ariel | Lambda Calculus | None |
| 24 Sep | Thejas | Generalized Algebraic Datatypes (GADTs) | None |
| 01 Oct | Ariel | The Curry-Howard Isomorphism | None |
| 08 Oct | Jacob | Semantics and Logic | HW07 |
| 15 Oct | Cam | Subtyping | HW08 |
| 22 Oct | Thejas | Higher-Order Abstract Syntax (HOAS) | None |
| 29 Oct | Cam | Algebraic Effects | None |
| 05 Nov | Jacob | Category Theory | None |
| 12 Nov | Jacob | Cartesian Closed Categories | HW12 |
| 19 Nov | Cam | Dependent Types | HW13 |
| 26 Nov | Nobody | No Lecture | None |
| 03 Dec | Jacob | Homotopy Type Theory (HoTT) | None |
StuCo policy states that if you miss more than two classes, we cannot give you a passing grade for the class.
You cannot pass the class without completing most homeworks. If you skip more than two one-week homeworks or one two-week homework, you will not pass the class. If you miss a homework for any reason, contact the instructors for an extension and we'll give you time to make it up.
Homeworks are mandatory, but they are graded for effort, not correctness. This means that you must attempt to correctly complete every homework, but if you put in a good faith effort and do not manage to finish it correctly, you will still recieve credit.
Examples of homeworks that will recieve credit: A written homework with no problems solved correctly but all showing some work, a coding homework that has a substantial amout of relevant code but does not compile or does not pass tests, etc.
Examples of homeworks that will not recieve credit: A couple of words scribbled on a piece of notebook paper at the start of class, a coding assignment with only the starter code turned in, a coding assignment with no relevant code written, etc.
Please do not cheat.
Discussion of homework questions is always permitted in any form. However, direct copying of answers, whether code or written, is not permitted.