98-317: Hype for Types


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.

Fall 2019 Schedule

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 TBD
26 Nov Nobody No Lecture None
03 Dec Jacob Homotopy Type Theory (HoTT) TBD



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.

Academic Integrity

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.