Implementing a type theory with primitives for subtyping
Master Project

Project Description

This project is about implementing the type theory developed in “A Type Theory for Comprehension Categories with Applications to Subtyping”

In that paper, we develop a type theory that has built-in primitives for coercive subtyping.

The goal of this project is to implement the type theory, either in a computer proof assistant (Rocq, Agda, Lean, or other) or in a programming language such as Haskell or Ocaml - according to the preferences of the student. In the first case, the goal is to prove properties of the type theory. In the second, the goal would be to have a practical, usable implementation.

Links:

• The paper is available at https://arxiv.org/abs/2503.10868

Project Goals

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

• Learn the basics of Martin-Löf type theory (and its categorical semantics, if you want)
• Understand the type theory developed in “A Type Theory for Comprehension Categories with Applications to Subtyping” (and its categorical semantics, if you want)
• Option 1: Learn to use a computer proof assistant
• Option 2: Learn how to implement a type theory in a functional programming language

Contacts for the Project

• Benedikt Ahrens (TU Delft)