Nominal techniques as an Agda library

TL;DR

This paper explores an attempt to make nominal techniques accessible as an Agda library and aims for a technical victory of implementing nominal ideas and a moral victory that the overhead be acceptable for practical systems.

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