Type Theory

Created: Mar 06, 2018 by Pradeep Gowda Updated: May 29, 2020

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

• Row Polymorphism Isn’t Subtyping - BAM Weblog

• typing - What are the major differences between row polymorphism and subtyping - Computer Science Stack Exchange

• Objects and Aspects: Row Polymorphism – Neel Krishnaswami

Misc

• types.markdown and discussion