Well-Scoped Locally Nameless Representation of Syntax
This work provides a practical and verified representation technique for mechanizing languages with binders in proof assistants like Agda.
The authors advocate for a well-scoped locally nameless representation of syntax in dependent type theory, provide generic code parameterized by binding signatures in Agda, and prove its adequacy with respect to nameful syntax modulo alpha-conversion.
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.