98-317: Hype for Types - Fall 2019


This is a static page for the Fall 2019 semester of 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. See here for the (active) main page of the course.

The Fall 2019 instance of Hype for Types was 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

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 None
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 homeworks, 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.