When using interactive theorem provers based on dependent type theory to define and reason about languages involving binding constructs, we advocate the use of a well-scoped version of the locally nameless method of representing syntax. This paper describes generic code parameterized by a Plotkin-style binding signature for this style of syntax representation within the Agda theorem prover, gives a proof of its adequacy with respect to naive nameful syntax modulo alpha-conversion and discusses some examples of its use.

翻译：在使用基于依赖类型理论的交互式定理证明器来定义和推理涉及绑定结构的语言时，我们主张采用一种具有良好作用域（well-scoped）的局部无名称（locally nameless）语法表示方法。本文描述了在Agda定理证明器内，针对这种语法表示风格，通过Plotkin风格绑定签名参数化的通用代码，给出了其相对于朴素命名语法（模alpha转换）的适当性证明，并讨论了其使用的一些示例。