Topics in Dependent Type Theory

Topics in Dependent Type Theory


Event in April

If you want to get a taste of (homotopy) type theory, you can consider to attend (part of) two events on this subject taking place in building 200A on Apr 2-5, 2024:

Attendance is free. If you plan to attend full days, we ask to register for organizational reasons.

Dependent Type Theory

Martin-Löf type theory (MLTT) [ML82, ML84] is a formal system introduced by Per Martin-Löf as an alternative to set theory. MLTT can serve both as a logic and as a programming language. These two aspects are seamlessly combined in a single formalism using the Curry-Howard correspondence, which encodes propositions as program types, and proofs as programs of the appropriate type. For example,

As a logic, MLTT can replace Zermelo-Fraenkel set theory as a foundation for mathematics. In other words, it is possible to express general mathematical theorems and proofs within MLTT, and the expressive power of MLTT is similar to that of set theory. However, MLTT has a number of advantages, compared to set theory:

As a programming language, it has the advantage that it can check safety and correctness of programs at compile-time. This is achieved by running a type-checker (which is the exact same algorithm as the proof-checker mentioned above), which will verify

MLTT is part of a broader family of foundational mathematical theories called dependent type theories. Examples of dependently typed proof assistants include Agda, Coq (to be renamed to Rocq), Lean and Idris. A more exhaustive list is found on Wikipedia. Those systems are also called proof-assistants, as the user may input a proof (a computer program) interactively, that is, with constant feedback from the type-checker.

Equality in Type Theory

Equality is an important topic of interest in type theory. We distinguish two forms of equality:

The fact that we have an identity type a ≡ b for a, b : A (a and b of type A) means that we can consider objects p : a ≡ b of the identity type, called equality/identity proofs. One wonders how we should think and reason about these. First, we should note that these proofs have a role not only in further proving activities but also in programming. Indeed, if T(x) is a type dependent on x : A and we have a proof p : a ≡ b, then we are allowed to convert programs of type T(a) to programs of type T(b), via a function subst(T)(p) : T(a) -> T(b) (as present in both the Agda standard library and the Agda cubical library). However, since the types T(a) and T(b) may not be definitionally equal, they may classify different programs, and as such, the conversion function subst(T)(p) : T(a) -> T(b) actually has to perform a computation. This computation needs to be derived from T and p, so p is not just a proof of a fact, but actually carries the computationally relevant information about how to get from a to b.

There are several takes on what an equality proof is:

Universal Algebra and Programming Languages

Universal algebra is the study of algebraic theories without commiting to a specific one (such as group theory). An algebraic theory can be specified by listing a number of operations, each with an arity, and a number of equations.

When we specify an algebraic theory, we get:

The framework of algebraic theories is of interest to mathematics, but also to the study of programming languages and proof assistants. Models of a programming language can be denotational models in which we study a logic’s soundness (a.k.a. consistency), but remarkably, important parts of a programming language implementation such as a type-checker and a compiler can also be made to fit the definition of a model/algebra of an algebraic theory and this turns out to be a good way to structure the implementation’s source code [AACMM21, FS22].

Possible Subjects

We propose the option to work on a master thesis related to the concepts above, and including formalization work in Agda --cubical, likely leading to contributions to the standard cubical library.

A thesis on these subjects can be written in either Dutch or English.

Relevant courses

Courses particularly relevant here (but not indispensable) are:

Further reading

Relevant resources can be found here.


This is the list of references that are appropriate in the text above, but the cited papers are not necessarily the best point to start reading. See “Further reading” above instead.