Supervisors:
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 computing evidence. 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 (which is being 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.
We propose the option to work on a master thesis in the area of dependent type theory, and including formalization work in Agda, Lean or Coq/Rocq, possibly leading to contributions to the library ecosystem of these languages. Some relevant concepts are further introduced below.
--cubical or Lean. There are currently formalizations of SOMATs in plain Agda (using a possibly unnecessary detour where presheaves are represented as □-coalgebras) and MATs in Cubical Agda.--cubical) as a metatheory. This should simplify parts of the existing implementation, and non-Sikkel-specific concepts would be contributed to the cubical library.--cubical as contributions to the cubical library.A thesis on these subjects can be written in either Dutch or English.
Equality is an important topic of interest in type theory. We distinguish two forms of equality:
G with neutral element e, if we know that a^5 = e and a^7 = e, then we can conclude that a = e, but this does not follow simply from unfolding definitions. We call this propositional equality and, being a proposition, it is encoded by a type a ≡ e called the identity type. Propositional equality is strictly weaker than definitional 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:
In intensional type theory (ITT), propositional equality is essentially just the congruence generated by all equalities currently assumed. As such, after all these assumptions have been proven, it must be the case that propositionally equal values are in fact definitionally equal, so that any equality proof is ultimately refl: the proof that propositional equality is reflexive. Then subst(T)(refl) is simply the identity.
Problematically, function extensionality – the fact that pointwise equal functions are equal – is not provable in ITT and is therefore often assumed without proof. But this means that there is an object funext whose existence has been postulated without providing computational content, and which is never instantiated with a concrete value. As such, conversion along equalities proven using funext will block.
In homotopy type theory (HoTT) [Uni13], propositional equality just means isomorphism, and equality proofs are in 1-1 correspondence with isomorphisms. As there are many more isomorphisms than reflexivity proofs, a computational theory of HoTT will be more complex than one of ITT. Early versions of HoTT would simply block on certain axioms, but cubical type theory [CCHM15] is a type system that extends HoTT and fully computes. It derives its name from the fact that it has a semantics in cubical sets (presheaves over the “cube category”). With the option --cubical enabled, Agda acts as a proof assistant for cubical type theory [VMA21]. A relatively extensive standard library containing a significant module for category theory exists for Agda --cubical.
XTT [SAG22] is a type system in which equality proofs are regarded as in ITT, but it uses techniques from cubical type theory to allow computation with equality proofs even before they reduce to refl. Moreover, function extensionality is provable in XTT. For these reasons, we regard XTT as currently the most convenient system to work in when we care about computation, but do not need the full power of HoTT. To our knowledge there is currently no proof assistant for XTT, but it is sufficiently close to cubical type theory that we can simply use Agda --cubical.
The Lean proof assistant has its own take on equality, and may have benefits similar to XTT.
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.
Hom(x, y) for every two objects x and y, but also dependently typed programming languages.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].
Courses particularly relevant here (but not indispensable) are:
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.