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

翻译：名义化技术为处理编程语言中的名称与变量绑定问题提供了数学原理严谨的方法。本文探讨了将名义化技术实现为Agda库的尝试。我们旨在实现名义化思想的技术性突破，并进一步追求道德层面的胜利——确保该技术在实际系统中的开销处于可接受范围。本文的研究成果已完成机械化验证，并通过 https://omelkonian.github.io/nominal-agda/ 公开访问。