Representing variables and scopes for Agda Core

Jesper Cockx

The goal of the Agda Core project is to ensure the trustworthiness of Agda by means of a small core language that is deeply embedded in Agda itself. I also intend to explore its potential as the basis for meta-programming and proof exchange with other languages. As the first step in the development of Agda Core, I am currently focusing on defining the syntax of Agda Core. In this seminar I would like to discuss the crucial question of how to represent variables, scopes, and binding structure of this syntax.

---

Previous: Soham Chakraborty | Robustness between Weak Memory Models
Next: t.b.a. | No seminar (Arjen's PhD defense on Thursday)