What are references for learning type theory?

Question

What could be a good set of references for starting to learn type theory? We can assume that the students have a computer science background but not specifically on functional programming or lambda calculus, and that they know propositional and first-order logic but not constructive logic or proof theory (natural deduction or sequent calculi).

Answer 1

First, "type theory" is a broad concept encompassing many kinds of type theories and many use cases. For example, since this is the Proof Assistant Stack Exchange, there are two main kinds of type theories used for proof assistants:

• Simple type theory, including typed lambda calculus and Higher Order Logic (HOL): HOL is the basis for HOL-Light, HOL4, and Isabelle/HOL.
• Dependent type theory (DTT): DTT is the basis for Coq, Lean, Agda, Arend, and other proof assistants. Almost all of them use some variation on the Calculus of Inductive Constructions (CIC) which is a way to add computational rules to DTT to make it more automatic to generate some proofs. Also, a common extension of dependent type theory is Homotopy Type Theory (HoTT) which is used for some Coq projects, many Agda projects, and all of Arend. (Lean used to support HoTT, but mostly doesn't anymore.)

There are also many things you can do with type theory:

• Mathematics
  • Type theory is used practically to build proof assistants and prove theorems in math (as already mentioned above).
  • Type theory provides an alternative foundation of mathematics similar to set theory, but which more easily incorporates constructive logic and universe levels. Just like set theory, one can study the meta-logical properties of type theory such as its consistency and the properties of various extra rules and axioms (like univalence axiom and the axiom of choice).
  • Type theory provides a way to describe special kinds of categories in category theory, including Cartesian-closed categories and Topos categories, as well as their higher-category versions.
  • Conversely, category theory provides models of various type theories. (A major area of research is models of HoTT.)
• Computer science
  • Type theory provides a framework for practically building functional programming languages. Simple type theory provides the framework for statically typed functional languages like OCaml, Haskell, and Scala. DTT provides a framework for dependently types languages like Idris and Lean 4.
  • Type theories are closely related to computation, and as such there are a lot of computational questions about type theories such as if they compute or normalize. This is both theoretical, but also practical, since many theorem provers and programming languages use the computational properties of type theory and trust that terms in the language will reduce/compute and types in the language will type-check.
  • Just as there are categorical models to type theories, there are also computational models which describe the type theory as a programming language.

Having said all this, you can see that there isn't just one aspect to type theory, and maybe unlike logic, there isn't an established Introduction to Type Theory curriculum that I'm aware of.

Here are a few suggestions:

• Look at the The MathOverflow question Good Introductory Book to Type Theory? which is basically an older duplicate of this question.
• If you are interested in HOL, look at the question The Proof Assistant StackExchange question Reference request for an introduction to higher order logic.
• Since you are on the proof assistant stack exchange, I would just recommend starting by learning a theorem prover or two. Lean, Coq, and Agda would be good for learning DTT, and they have good tutorials. (For Lean 4, look at Theorem Proving in Lean 4. For HoTT in Agda, see Introduction to Univalent Foundations of Mathematics with Agda . For HoTT in Arend, see the Arend Tutorial.) Isabelle/HOL and HOL-Light have good tutorials for learning HOL. (For Isabelle/HOL, see Programming and Proving in Isabelle/HOL).
• My advisor, Jeremy Avigad, has written a logic book, Mathematical Logic and Computation. It covers (or will when it is released) both simple typed lambda calculus, as well as dependent type theory.
• The standard dependent type theory introduction is now the first chapter to The HoTT Book. This goes deeper into DTT than many theorem prover tutorials, and if you are interested in HoTT, you can read the rest of the book.
• If you are interested in learning about the duality between category theory and type theory, I've found Steve Awodey's Category Theory helpful, especially the section 6.6 on lambda calculus. After that, you can look at the article From Sets to Types to Categories to Sets.