Improving the Agda typechecker
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)
Supervisor(s): Jesper Cockx
Posted: October 25, 2022