Supervisor

Suitable for

Abstract

I am happy to supervise students at all levels who want to work on or with type theory. Types were originally introduced to stop programmers from writing bad code, but turned out to be an extremely fruitful positive idea. Modern systems like dependent type theory are powerful enough to both express intricate properties of programs and to formalise advanced mathematics, as demonstrated with theorem provers such as Agda, Coq or Lean.

The following give an idea what a project with me could look like:

• Solving monoidal categories: Monoidal categories offer a notion of tensor product which is both very general and concretely applicable. This project is about implementing a tool in Agda that can automatically construct morphisms in a monoidal category (possibly adding more morphisms than the structural morphisms). A student working on this project will get experience in dependent type theory, meta-programming in Agda, and monoidal category theory.
• Formalising programming language meta-theory: Dependent type theory allows for implementing and reasoning about other programming languages. The student can take a language of choice (for instance the lambda- or pi-calculus), represent it in a theorem prover, and then formally prove properties of that language or devise a verified compiler. This project is ideal for students interested in PL theory and Compilers.
• For students with a background in mathematics I am also open to supervise mathematical formalisation projects. For this it might be expedient to have another supervisor in mathematics who is an expert in the specific domain the student wants to formalise.

These are only suggestions, I am very happy for students to devise their own projects based on their background and interests.

 

Prerequisites: Principles of Programming Languages, Lambda Calculus and Types