Well-Scoped Locally Nameless Representation of Syntax
Logic in Computer Science
2026-05-12 v1
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.
Cite
@article{arxiv.2605.08990,
title = {Well-Scoped Locally Nameless Representation of Syntax},
author = {Andrew M. Pitts},
journal= {arXiv preprint arXiv:2605.08990},
year = {2026}
}
Comments
20 pages, 3 figures