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

• Jesper Cockx (TU Delft)