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

Computer formalization of Voevodsky's theory of type theories

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: June 05, 2022