Introductory materials
- Learn Type Theory
- Type Theory in 15 minutes [presentation in PDF].
Important concepts in type theory.
Alonzo Church's typed lambda-calculus -- mathematical foundation
Per Martin-Löf's intuitionistic type theory, 1998 :cite:martin1998intuitionistic
Curry-Howard correspondence -- equates programs with proofs.
Homotopy type theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.
Type inference
Type Inference by Solving Constraints – Caleb Helbling – Programming Languages & Systems
Videos
- "Type Theory Foundations" lecture by Robert Harper at OPLSS 2013.
To read
- "Programming in Martin-Lof's type theory" by Nordstrom, 1990 cite:[Nordstrom1990]
Row polymorphism vs subtyping
Objects and Aspects: Row Polymorphism -- Neel Krishnaswami