Representing variables and scopes for Agda Core

Jesper Cockx

Date: Wed, October 06, 2021
Time: 12:00
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.

Previous: Soham Chakraborty |
Next: t.b.a. |