98-317: Hype for Types


Hype for Types is a student-run course at CMU teaching topics in type theory and related disciplines. It is aimed at students with only basic knowledge of functional programming, and designed to give them a high-level introduction to a variety of fascinating topics which could otherwise only be learned after years of detailed study. Some topics that have been covered in Hype for Types include: typechecking, phantom typing, (generalized) algebraic datatypes, subtyping, lambda calculus, the Curry-Howard isomorphism, constructive logic, dependent type theory, category theory, Homotopy Type Theory, pure type systems, higher-order abstract syntax, algebraic effects, Hoare logic, parsing, and compilation.

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.


Spring 2020 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
14 January Jacob Welcome, Intro to Type Theory HW 01
21 January Cam Algebra, Calculus and Trees HW 02
28 January TBA TBA
04 February TBA TBA
11 February TBA TBA
18 February TBA TBA
25 February TBA TBA
03 March TBA TBA
17 March TBA TBA
24 March TBA TBA
31 March TBA TBA
07 April TBA TBA
14 April TBA TBA
21 April TBA TBA
28 April TBA TBA



We will be taking attendance at each lecture. StuCo policy states that if you miss more than two classes without prior notice, we cannot give you a passing grade for the class. So please let us know ahead-of-time if you cannot make it. Even if your absence is excused, you are still responsible for any homework assigned (see below). Please coordinate with that week's lecturer to get the content of the lecture, especially if lecture slides/notes are not posted.


For several of the lectures, we will be subsequently assigning homework to reinforce the content of the lecture and to give you additional practice with the topics covered. The homeworks are designed to follow readily from the lectures, and should not require a great amount of time or effort. As a general rule, you shouldn't be spending much more than half-an-hour on each homework assignment.

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.

We understand that you're busy and might not have time to complete the homework the week it's assigned. That's okay! If you're not able to complete an assignment within one week (i.e. by the next lecture), please email us (or post a private question to the instructors on Piazza) to get an extension. However, please stay on top of the homeworks! We reserve the right to deny you an extension if you have too many homeworks outstanding.

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.