Important concepts in type theory.
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 by Solving Constraints – Caleb Helbling – Programming Languages & Systems
Objects and Aspects: Row Polymorphism – Neel Krishnaswami