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.
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.
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.