A mechanically checked type checker
Master Project


Project Description

In this project, you develop a verified type checker for Martin-Löf type theory.

Similar projects are already underway, such as Metarocq. The goal of this project is to build a small-scale version, to understand the main principles of such verification.

Project Goals

In this project, you will work on the following goals:

  • Learn the basics of Martin-Löf type theory
  • Learn to use one computer proof assistant (Rocq, Agda, Lean, or other)
  • State and prove desirable properties of MLTT

Contacts for the Project


A mechanically checked type checker

Supervisor(s): Benedikt Ahrens
Posted: December 05, 2025