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