A type checker for directed type theory
This project is suitable for students with an interest in type theory and functional programming.
A type theory is a strongly typed (functional) programming language similar to Haskell or Ocaml.
It serves as a basis for computer proof assistants such as Agda and Coq. In a recent work (click here), Riehl and Shulman present a directed type theory (which allows to internalize infinity-categories, but this is not important for this project), a powerful, but complicated generalization of type theory.
The goal of this project is to write a type-checker for this directed type theory. More precisely, the programme to be written should take, as an input, two terms t and T and check whether “t : T” (read: t is of type T) holds. In a second step, the goal will be to write a function that, given a term t, returns a term T such that “t : T” holds (type synthesis).
This type checker could form the core of a proof checker for directed type theory.
Formalization of mathematics in univalent type theory
This project is suitable for students with an interest in dependent type theories and computer
proof assistants built on such type theories.
In the UniMath project (click here), a group of people are building a library of mathematical knowledge, called UniMath, where all proofs are formally checked by a computer program. The logical foundation of this computer program is type theory, an expressive (programming) language in which mathematical statements and proofs can be formulated, and subsequently checked by the computer.
In this project, we propose formulating and proving some result – to be chosen in accordance with the interests of the student – of mathematics or computer science in the UniMath library. Such a result could be, e.g.:
- The correctness of a sorting algorithm, i.e., programming the algorithm and showing that the output of the algorithm is always sorted.
- Error-correction properties of linear codes. This project involves implementing matrices and operations on them, as well as proving correctness of those operations.