Links to various good resources on how to learn and implement type theory. It is mainly on dependent type theory, because that’s what I’m interested in.

Theory

• I first learnt about type theory from Simon Thompson his book Type Theory and Functional Programming is an excellent introduction.
• learn-tt a collection of papers and resources on type-theory.

Implementation

• The Type Checker Zoo
• The Elaboration Zoo
• An excellent online lecture How to code your own type theory by Jon Sterling

Homotopy type theory

Homotopy type theory (HoTT) is a version of type theory with the Univalence Axiom where isomorphism of types implies equality. There are lots of good resources including:

• The HoTT Book
• Introduction to Homotopy Type Theory by Egbert Rijke. An earlier version can be found on arXiv.