Learning Structure-Aware Representations of Dependent Types

Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy

Agda is a dependently-typed programming language and a proof assistant, pivotal in proof formalization and programming language theory. This paper extends the Agda ecosystem into m…