Extending the Agda Core project

Extending the Agda Core project
Master Project

Project description

Dependently typed programming languages such as Agda can be used to specify and prove correctness of programs, thanks to the Curry-Howard correspondence between programs and proofs. However, to trust these proofs we also need to trust the implementation of the language itself. Hence one important goal of research into dependently typed languages is how to use these languages to verify the correctness of their own type checkers.

The goal of the Agda Core project is to provide a formal specification in Agda of a core language for Agda itself, plus a correct-by-construction type checker for it. At the moment, the implementation only covers a basic subset of the full Agda language, so the goal of this project is to extend it with one of the following features:

Dependent case analysis
Definitional proof irrelevance
Eta-equality for functions and record types
Lazy evaluation
Positivity checking for inductive datatypes
Termination checking for recursive functions
Universe polymorphism

In this project, you will not just to add to the existing implementation of Agda Core: you will also study the different techniques for formalizing dependently typed languages and implementing correct-by-construction dependent type checkers, using Agda Core as a lens for this study.