Type Theory#

Type theory provides a formal framework for reasoning about types and their relationships in programming languages.

Topics#

• Types
• Terms
• Judgements
• Rules of Inference
• Type Inhabitation
• Curry-Howard Correspondence
• Homotopy Type Theory
• Atomic Terms
• Function Terms
• Lambda Terms
• Function Application
• Reductions

Resources#

Books#

• Type Theory and Functional Programming by Simon Thompson
• Programming in Martin-Löf's Type Theory by Bengt Nordström, Kent Petersson, Jan M. Smith
• Homotopy Type Theory: Univalent Foundations of Mathematics by The Univalent Foundations Program

Online Resources#

• MIT: Type Theory
• Stanford: Type Theory
• CMU: Type Theory

Practice Problems#

• Type Theory Exercises
• Type Theory Problems
• Type Theory Challenges