Well-Scoped Locally Nameless Representation of Syntax

TL;DR

This paper proposes a well-scoped locally nameless syntax representation method within Agda, providing generic code and proofs of correctness for reasoning about languages with binding constructs.

Contribution

It introduces a well-scoped locally nameless approach for syntax representation in Agda, with generic code and formal adequacy proofs.

Findings

Provides a generic implementation of the syntax representation in Agda.

Proves the adequacy of the representation with respect to naive nameful syntax.

Includes examples demonstrating the method's application.

Abstract

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.