Nominal techniques as an Agda library
Programming Languages
2026-03-05 v1 Logic in Computer Science
Abstract
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 techniques accessible as an Agda library. We aim for a technical victory of implementing nominal ideas; we further require a moral victory that the overhead be acceptable for practical systems. The results of this paper have been mechanised and are publicly accessible at https://omelkonian.github.io/nominal-agda/.
Keywords
Cite
@article{arxiv.2603.03968,
title = {Nominal techniques as an Agda library},
author = {Murdoch J. Gabbay and Orestis Melkonian},
journal= {arXiv preprint arXiv:2603.03968},
year = {2026}
}