Supervisors:
Other contact person: see different topics
Martin-Löf type theory (MLTT) 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.
As a logic, it 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. Besides, 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 implementations of such dependent type theories (i.e. type-checker implementations) include Agda, Coq, Lean, 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.
A master thesis in dependent type theory can take various directions. We sketch a couple below, but input from prospective students who may have their own interests within the research domain, is encouraged both before the start of the master thesis and during the initial literature study phase.
Contact: antoine.vanmuylder@kuleuven.be
In 1930 Kurt Gödel established the existence of a general mathematical phenomenon regarding foundational mathematical theories T (T = MLTT, set theory, Peano arithmetic, …). Basically, if T can encode a basic form of arithmetic, and if T proves no contradictions, then some propositions that T can formulate are neither provable, nor refutable by T. Such propositions are then dubbed independent of T.
For example, let us consider T = ZFC. The continuum hypothesis is a proposition that we can formulate in ZFC, asserting: “There is no set whose cardinality is strictly between that of the integers and the real numbers”. Paul Cohen proved in 1963 that this formula is in fact independent from ZFC.
Since MLTT has a logical power roughly equivalent to that of ZFC, one could think that Gödel’s theorem applies here too. It is indeed the case, and independents of MLTT include very simple statements, such as function extensionality. This proposition asserts that pointwise equality of functions implies equality of functions. Note the Type quantification, and the higher-order quantification: MLTT allows us to quantify a statement on types and on typed functions. This is already quite different from what we would write in ZFC. The column symbol “:” stands for “is of type” and can be understood as a replacement for “∈”.
∀ (A B : Type), ∀ (f g : A → B), (∀ (a : A), f a ≡ g a) ↔︎ f ≡ g.
Here is another, though arguably more abstruse, independent statement of MLTT called univalence (coined by Vladimir Voevodsky in ≈ 2003, based on earlier ideas by Streicher, Hofmann).
∀ (A B : Type), (A ≃ B) ↔︎ (A ≡ B).
Univalence asserts that isomorphic types may be considered as equal, i.e. are interchangeable. Roughly speaking, univalence conveniently formalizes a form of representation independence. The latter principle is used day-to-day by mathematicians and we explain it here with an example. Suppose you equip an abelian group X = (X,+,0) with a ring structure (multiplication satisfying the ring laws…). At a later point in time, you discover that another abelian group Y = (Y,+,0) is isomorphic to X, i.e. X ≃ Y. Univalence, and the type-theoretic setting let you build with no mathematical overhead costs a ring structure for Y: in a proof assistant, building this structure for Y would consist of a single line of code, mentioning the univalence axiom. In set theory, you would need to prove an extra explicit congruence theorem, stating that having a ring structure is invariant under isomorphisms of the underlying additive group. Univalence grants a completely generic proof of the latter fact, and is therefore more generally of great help when it comes to formalizing mathematics.
In the field of logic, it is an interesting and difficult task to study what kind of extra logical rules could entail specific independent statements.
Of course, one possibility is to assume the statement of interest as an additional axiom. This is the approach taken by the book Homotopy type theory - Univalent Foundations of Mathematics (the “HoTT book”) for univalence, as advocated by Voevodsky. This book features a dependent type theory extending MLTT with additional axioms, including the univalence axiom. However, in dependent type theory, assuming axioms can be unsatisfactory from a computational/constructive point of view, since these axioms have unspecified computational behaviour. In the example above, the multiplication operation we built for Y by assuming univalence mentions this axiom in its very definition, so it will not actually compute, and it would be up to us (*) to rephrase this structure as a more conventional ring if possible.
Cubical type theory is an extension of MLTT that solves the above problem. It features, for any type A, a new type called Path A whose elements (paths between elements of A) are supposed to account for a built-in notion of isomorphism. Indeed, cubical type theory enforces extra rules that make paths behave as isomorphisms. For instance it specifies how to compose paths, or reverse paths. As an example, the type Path Grp of paths between groups can be proven isomorphic to the type of group isomorphisms, using the rules of cubical type theory. Those rules can be used to derive univalence (as a theorem with computational behaviour), and proofs of the form (*) then become much easier, if not unnecessary. Note that the name Path purposedly refers to topological paths: in fact the whole syntax of cubical type theory can be mapped to topological constructs, following the idea that types (from cubical type theory) are syntax for homotopy types (equivalence classes of topological spaces under homotopy). That is why cubical type theory constitutes what is called a homotopy type theory (HoTT).
The first challenge of this thesis topic will be to gain familiarity with functional programming and dependent type theory, and cubical type theory in particular. For this you will work with the Agda cubical proof assistant (or custom extensions).
Even if cubical type theory decides more mathematical statements than MLTT (e.g. univalence), it is still subject to Gödel incompleteness, and some independents are still very simple to formulate. Here are some Church encodings:
On one hand, set theory refutes this kind of statements. Written in a more set-theoretic fashion, the first statement would look like Π_(X ∈ Set) Fun(X,X) (let us pretend that the collection of all sets Set is a set for a split second…). You can certainly think of 2 different inhabitants of this product. On the other hand, some extensions of cubical type theory validate those statements. Those theories add type-theoretic rules that more or less remove the possibility of “an if-then-else statement for types”. Consequently, when building an element of ( ∀ (X : Type), X → X ) in those theories, you have no choice but to input an identity function. Such extensions of dependent type theories are called Parametric type theories.
The second challenge of this topic will be to understand precisely what parametricity is (in one sentence: invariance under relations), and explore its consequences. For this you will be working with Agda bridges, an extension of the cubical Agda proof assistant designed and implemented at KU~Leuven that adds parametricity to the theory.
agda --cubical (agda installation instructions). Note: It’s easier to install agda on a linux machine. Here is some material related to agda --cubical:
Contact: joris.ceulemans@kuleuven.be
As discussed in the previous section, MLTT can be extended with various new primitives or reasoning principles that allow a user to write more programs or prove more theorems. Other examples include guarded recursive type theory (which introduces new primitives for programming with/reasoning about infinite data structures in a principled way) or nominal type theory (which provides primitives for working with names when formalizing the syntax and metatheory of other programming languages within a proof assistant). Of course, since we want to use dependent type theory as a logic, we must make sure that adding new reasoning principles to MLTT does not lead to a contradiction (i.e. that we obtain a system in which every statement is provable). This is typically done by constructing a mathematical model in which the proposition False is interpreted as the empty set. To see that this proves soundness, one can observe that a proof of False in the type theory would give rise to the construction of an element of the empty set.
Many of the extensions described above only exist on paper as a formal system. However, we want to take advantage of the newly added primitives and actually use them in a proof assistant. One approach to do this, is to develop a new proof assistant or to adapt the source code of an existing proof assistant. An example of the latter category is the above mentioned Agda bridges, which has been built on top of Cubical Agda and which provides new primitives for reasoning with parametricity. An advantage of this approach is that one can intervene in any phase of the type checking process (e.g. parsing, the actual type checking, error message generation) and as a result obtain a proof assistant with a very convenient interface to the end user.
An alternative approach that we are currently investigating is the development of a library for type theory extensions written within an existing proof assistant. This is based on the observation that MLTT can serve as a foundation of mathematics, and as a result we can formalize within MLTT the mathematical models behind the extensions we are interested in. This research has led to the Sikkel library (see here for the Agda code), which is built around an Agda formalization of a broad class of categorical models of type theory known as presheaf models. Such a presheaf model is parametrized by a so-called base category, and depending on that base category the model allows us to interpret different type theory primitives. In this way Sikkel has been instantiated to provide support for guarded recursion, a limited form of parametricity and a form of nominal types.
An advantage of the library approach is that we never actually leave the original proof assistant (Agda in the case of Sikkel). This allows us to use type theory extensions in a modular way: a programmer only needs to use Sikkel for those parts of the program that genuinely rely on the primitives offered by the extension. It is also possible to instantiate Sikkel with different extensions in different parts of the same Agda development. This stands in contrast with writing an entire project in a purpose-built proof assistant that implements one type theory extension. Another benefit of Sikkel is that soundness is immediate since every Sikkel program is directly interpreted in the formalized model.
Depending on the student’s interest, a master thesis about Sikkel can focus on different topics. We include two examples below, but students may also come up with other interesting topics during the literature study.
Guarded recursive type theory is one of the extensions that has currently been worked out in Sikkel. As mentioned above, it is used to program with infinite data structures in a principled way. At the moment, only infinite streams have been studied in Sikkel, but the model is expressive enough to interpret other data structures like trees. A possible master thesis topic is the extension of the current Sikkel support for guarded recursion to cover a class of infinite data structures, of which streams and trees will form an instance, and spell out how these general structures can be interpretd in the model. An ambitious student might continue to expand the class of data structures to also cover a domain for the interpretation ocf the untyped lambda calculus.
The currently released version of Sikkel only supports simple types, although its model is already dependently typed. This means that at the moment, Sikkel users can only write programs but not prove properties of these programs. A logical framework for Sikkel, which allows users to state and prove properties of Sikkel programs and which interprets the proofs in a presheaf model, is currently under construction and is in a final phase of its development. In a master thesis a student can investigate the strengths and weaknesses of this framework by proving considerable theorems in it, e.g. results about programs written in a nominal type theory. Before doing so, a student will have to extend the logical framework and proof system with new connectives that are specific for the considered extension.