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

Improving the Agda typechecker

Supervisor(s): Jesper Cockx
Posted: October 25, 2022