2 papers
cs.PL2026
Nominal techniques as an Agda library
Murdoch J. Gabbay, Orestis Melkonian
Nominal techniques provide a mathematically principled approach to dealing with names and variable binding in programming languages. This paper explores an attempt to make nominal…
cs.LG2024
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…