Nominal techniques as an Agda library

arXiv (Cornell University) 2026 Preprint Open access

Read full text
Authors: Murdoch J. Gabbay, Orestis Melkonian
DOI: 10.48550/arxiv.2603.03968
Cited by: 0

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/.

Fields of Study & Subjects

Logic programming and type systems semigroups and automata theory Syntax Semantics Linguistic Variation

Publication details

Journal / source
arXiv (Cornell University)
Publication date
4 March 2026
Language
EN
Document type
Preprint