Computer formalization of Voevodsky's theory of type theories
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:
- to give a precise mathematical definition of what a “type theory” is
- 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.
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
Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: June 05, 2022