Improving the Agda typechecker
Master Project

Project description

This is not a concrete project but rather a collection of possible ideas related to the implementation of the dependently typed language and proof assistant Agda. Possible topics for a thesis project include:

• The design of a type system that can enforce that certain functions are run-time identity functions, and can thus be removed during compilation.

• Cumulativity in Agda: design and implement a solver for universe level constraints that guarantees minimal solutions.

• Incremental compilation of pattern matching definitions to a case tree.

• Better mechanisms for controlling when definitions should or should not be unfolded in the type checker.

• Improving Agda’s error messages by keeping track of the origin of metavariables.

• …

Contacts for the project

• Jesper Cockx (TU Delft)