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.

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

  • 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