Nominal techniques as an Agda library

TL;DR

This paper presents an Agda library implementing nominal techniques for handling names and variable binding, aiming for both technical correctness and practical usability, with results available publicly.

Contribution

It introduces a formalized Agda library for nominal techniques, making these concepts accessible and usable in practical formal systems.

Findings

Successfully mechanized nominal techniques in Agda

Library is publicly accessible online

Achieved a balance between correctness and practicality

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