Computer formalization of Voevodsky's theory of type theories
Master Project

Project Description

In the last years of his life, Fields Medalist Vladimir developed a mathematical theory of type theories. The main purpose of this theory is twofold:

1. to give a precise mathematical definition of what a “type theory” is
2. to give a mathematical justification of recursion on the syntax of a type theory

Recursion on syntax is used to define interpretations of the syntax into worlds of mathematical objects.

When he passed away, Voevodsky left behind a large body of work, a significant part of it unfinished, on his theory of type theories. Voevodsky’s dream was to implement his theory in a computer proof assistant. To this end, his papers are in what he calls “formalization-ready” style, giving much more detail than traditional mathematics articles.

The goal of this project is to implement, in some computer proof assistant (Coq, Lean, Agda, Isabelle,…), a piece of Voevodsky’s mathematical theory.

Project Goals

In this project, you will work on (some of) the following goals:

• Learn to use one or more computer proof assistants, e.g., Coq, Agda, Lean, Isabelle
• Understand a part of Voevodsky’s theory of type theories
• Implement Voevodsky’s definitions and proofs, possibly filling in gaps

Contacts for the Project

• Benedikt Ahrens (TU Delft)
• Kobe Wullaert (TU Delft)