98-317: Hype for Types

hypefortypes.github.io · 1,630 words · saved by 1 readers

Hype for Types is a student-run course (StuCo) at CMU teaching topics in type theory and related disciplines. It is designed to give students a high-level introduction to a variety of fascinating practical topics in type theory and programming language theory which could otherwise only be learned after years of detailed study. Some topics that have been covered in Hype for Types include: typechecking, lambda calculus, the Curry-Howard isomorphism, constructive logic, dependent type theory, category theory, Homotopy Type Theory, pure type systems, higher-order abstract syntax, phantom typing, (generalized) algebraic datatypes, subtyping, algebraic effects, Hoare logic, parsing, and compilation. This course is aimed at students with a basic knowledge of functional programming, such as experience in Standard ML, OCaml, or Haskell. We will often use Standard ML in lectures and on homework assignments. It is currently taught by: Subject to change. After each lecture, the relevant notes/slid

98-317: Hype for Types 98-317: Hype for Types About Hype for Types is a student-run course (StuCo) at CMU teaching topics in type theory and related disciplines. It is designed to give students a high-level introduction to a variety of fascinating practical topics in type theory and programming language theory which could otherwise only be learned after years of detailed study. Some topics that have been covered in Hype for Types include: typechecking, lambda calculus, the Curry-Howard isomorphism, constructive logic, dependent type theory, category theory, Homotopy Type Theory, pure type syst

98-317: Hype for Types

related reading