Tactics for Substitution in Agda


NOTE: This project is already taken (2021).

Agda[1] is often used to represent the syntax of programming languages
with binding through inductive types or families, often represented by
De Bruijn indexes.

A common problem is then to implement substitution and a few basic
theorems about it for these term representations. Quite a few
alternatives have been proposed over the years, but none that ended up
being clearly more convenient than just a direct implementation of
substitution for the specific language at hand.

This proposal is about using the recently obtained reflection
capabilities [2] of Agda to define substitution and associated theorems
automatically with a tactic. The agda-prelude library [3] has many
examples of how to use reflection in Agda.

The autosubst [4] Coq library is a good example of the kind of
automation that we would be aiming for. However aside from the
difference in the tactic language, Agda developements also tend to use
intrinsically typed syntax, which would pose an additional challenge.

[1] http://agda.readthedocs.io
[2] http://agda.readthedocs.io/en/latest/language/reflection.html
[3] https://github.com/UlfNorell/agda-prelude
[4] https://www.ps.uni-saarland.de/autosubst/

Date range: 
September, 2019 to September, 2021