Representing variables and scopes for Agda Core
Date: Wed, October 06, 2021
Room: Jesper's zoom room
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.