arxiv: 2605.08990 · v1 · submitted 2026-05-09 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

Well-Scoped Locally Nameless Representation of Syntax

Andrew M. Pitts

Pith reviewed 2026-05-12 01:47 UTC · model grok-4.3

classification 💻 cs.LO

keywords locally namelesswell-scopedAgdabinding signaturesalpha-conversionsyntax representationdependent type theory

0 comments

The pith

Well-scoped locally nameless syntax in Agda is adequate for nameful syntax modulo alpha-conversion

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper presents a method for representing syntax with binding constructs using a well-scoped locally nameless approach in dependent type theory. Generic code is provided in Agda that is parameterized by Plotkin-style binding signatures. A proof shows this representation is adequate compared to the naive nameful syntax under alpha-conversion. Such a representation helps in interactive theorem proving by managing binders without manual handling of names and equivalences. If the claim holds, it enables more reliable formalizations of languages involving variable binding.

Core claim

The paper describes generic code parameterized by a Plotkin-style binding signature for a well-scoped version of the locally nameless method of representing syntax. It gives a proof of its adequacy with respect to naive nameful syntax modulo alpha-conversion and discusses some examples of its use.

What carries the argument

Well-scoped locally nameless representation, a syntax encoding that uses de Bruijn indices for bound variables and named free variables while enforcing scoping at the type level to prevent invalid terms

If this is right

Users can define syntax for languages with binders in Agda using the generic code for any Plotkin-style signature.
The adequacy proof ensures that reasoning in the locally nameless representation corresponds to reasoning up to alpha-equivalence in the nameful version.
Examples demonstrate practical application to common binding constructs.
The parameterization supports reuse across different language definitions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This method could be ported to other interactive theorem provers that support dependent types.
It might reduce the overhead of proving substitution lemmas by leveraging the well-scoped property.
Further work could test the approach on more complex signatures with multiple binding operators.

Load-bearing premise

The generic code correctly implements the well-scoped locally nameless representation for arbitrary Plotkin-style binding signatures and the adequacy relation holds after parameterization.

What would settle it

A specific example of a binding signature where some term in the locally nameless representation does not correspond to any alpha-equivalence class in the nameful syntax, or vice versa, would show the adequacy proof fails.

Figures

Figures reproduced from arXiv: 2605.08990 by Andrew M. Pitts.

**Figure 2.** Figure 2: Typing rule for natural number elimination in “exists-fresh” form [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗

**Figure 3.** Figure 3: Cofinite typing rule for natural number elimination [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Pitts has built a reusable, machine-checked Agda library for generic well-scoped locally nameless syntax with an adequacy proof against ordinary nameful syntax.

read the letter

This paper supplies generic Agda code for well-scoped locally nameless representations of syntax, parameterized over Plotkin-style binding signatures, plus a machine-checked proof that the representation is adequate for naive nameful syntax modulo alpha-conversion. The formalization is the core contribution and the main reason to pay attention. Because everything is checked in Agda, the adequacy claim rests on actual code rather than an informal argument, which removes the usual worry about gaps in binding lemmas. The parameterization is also useful: once the library is in place, different languages can instantiate it without repeating the binding infrastructure. The abstract mentions examples of use, which at least shows the code is meant to be applied rather than left as a theoretical exercise. The adequacy relation is defined against an external notion of syntax, so there is no circularity in the statement. On the practical side, the well-scoped restriction should make some operations simpler than the classic locally nameless approach, though the paper does not quantify any performance or proof-size overhead that might come with the generic setup. No load-bearing assumptions appear to be hidden; the development is presented as a self-contained library. This work is aimed at people already using Agda or similar dependently typed provers to formalize languages with binders. If you are in that group, the library could cut down on duplicated effort across projects. It is solid enough on the formal side to merit sending out for peer review rather than desk rejection; referees can check the Agda files directly and assess how easy the parameterization is to use in larger developments.

Referee Report

0 major / 3 minor

Summary. The manuscript presents generic Agda code, parameterized over Plotkin-style binding signatures, for well-scoped locally nameless representations of syntax with binding. It supplies a machine-checked adequacy theorem relating the representation to an independently defined nameful syntax modulo alpha-conversion and illustrates the approach with examples.

Significance. If the formalization holds, the work supplies a reusable, verified library for handling binders in dependent type theory, a recurring pain point when formalizing languages and logics. The machine-checked adequacy proof against an external nameful definition is a clear strength, as is the parameterization over arbitrary binding signatures and the emphasis on well-scoped representations that avoid common de Bruijn or name-related errors.

minor comments (3)

The abstract states that the code is 'generic' and 'parameterized by a Plotkin-style binding signature,' but the main text would benefit from an early, self-contained example of a concrete signature (e.g., for lambda calculus) together with the corresponding Agda type declarations to make the parameterization concrete for readers unfamiliar with Plotkin signatures.
Section 3 (or the adequacy theorem statement) should explicitly record the precise inductive definition of the adequacy relation and the induction hypotheses used in the proof; while the machine-checked development is authoritative, a compact informal statement in the paper would improve readability without duplicating the formal code.
The discussion of examples would be strengthened by a short table comparing the size or complexity of the well-scoped locally nameless terms versus the nameful versions for at least one non-trivial example, to illustrate the practical overhead.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and significance assessment of our manuscript on well-scoped locally nameless syntax. We are pleased that the generic Agda development, parameterization over Plotkin-style binding signatures, machine-checked adequacy theorem, and illustrative examples are viewed as a strength for formalizing languages with binders in dependent type theory.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper supplies a machine-checked Agda formalization of generic well-scoped locally nameless syntax parameterized over Plotkin-style binding signatures, together with an explicit adequacy theorem relating it to an independently defined nameful syntax modulo alpha-conversion. The central claim rests on the correctness of that formalization and the external definition of nameful syntax rather than on any self-referential definition, fitted parameter renamed as prediction, or load-bearing self-citation chain. No equations or steps in the provided description reduce the result to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard background notions of binding signatures and alpha-equivalence; no new free parameters or invented entities are introduced.

axioms (2)

domain assumption Plotkin-style binding signature
The generic code is parameterized by such signatures as stated in the abstract.
standard math Alpha-equivalence on nameful syntax
Adequacy is stated with respect to this standard equivalence.

pith-pipeline@v0.9.0 · 5352 in / 1200 out tokens · 48863 ms · 2026-05-12T01:47:08.401898+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat (inductive zero/step structure) unclear
The type Trm[ n ] of n-terms ... i : Fin n → Trm[ n ], a : A → Trm[ n ], o : (op : Op Σ) → Arg[ n ] (ar Σ op) → Trm[ n ] (Definition 4.2)
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear
adequacy ... bijection between Trm and α-equivalence classes of nameful terms (Proposition 5.5)

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages · 1 internal anchor

[1]

Abel.Normalization by Evaluation: Dependent Types and Impredicativity

A. Abel.Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, may 2013

work page 2013
[2]

A. Abel, N. A. Danielsson, and O. Eriksson. A graded modal dependent type theory with erasure, formalized.ArXiv e-prints, arXiv:2603.29716 [cs.LO], 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[3]

A. Abel, J. Öhman, and A. Vezzosi. Decidability of conversion for type theory in type theory.Proc. ACM Program. Lang., 2(POPL), December 2017

work page 2017
[4]

Altenkirch, M

T. Altenkirch, M. Hofmann, and T. Streicher. Categorical reconstruction of a reduction free normalization proof. In D. Pitt, D. E. Rydeheard, and P. T. Johnstone, editors,Category Theory and Computer Science, pages 182–199, Berlin, Heidelberg, 1995. Springer

work page 1995
[5]

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanised metatheory for the masses: The POPLmark challenge. In J. Hurd and T. Melham, editors,18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, volume 3603 ofLecture Notes in Compu...

work page 2005
[6]

B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering for- mal metatheory. InProceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’08, page 3–15, New York, NY, USA, 2008. Association for Computing Machinery

work page 2008
[7]

Berger and H

U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed𝜆- calculus. In6th Annual Symposium on Logic in Computer Science, pages 203–211. IEEE Computer Society Press, Washington, 1991

work page 1991
[8]

Charguéraud

A. Charguéraud. The locally nameless representation.Journal of Automated Reasoning, 49(3):363–408, 2012

work page 2012
[9]

Cockx, D

J. Cockx, D. Devriese, and F. Piessens. Pattern matching without K. InProceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pages 257–268, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2873-9

work page 2014
[10]

T. Coquand. Pattern matching with dependent types. In B. Nordström, K. Petersson, and G. D. Plotkin, editors,Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, pages 66–79, June 1992

work page 1992
[11]

M. L . Daggitt, G. Allais, J. McKinna, A. Abel, N. Van Doorn, J. Wood, U. Norell, D. O. Kidney, and S. Meshveliani. The Agda standard library: Version 2.0.Journal of Open Source Software, 10(116):9241, 2025. 18

work page 2025
[12]

N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem.Indagationes Math- ematicae, 34:381–392, 1972

work page 1972
[13]

de Moura and S

L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, pages 625–635. Springer International Publishing, 2021

work page 2021
[14]

M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In14th Annual Symposium on Logic in Computer Science, pages 193–202. IEEE Computer Society Press, Washington, 1999

work page 1999
[15]

Semantic analysis of normalisation by evaluation for typed lambda calculus

Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Mathematical Structures in Computer Science, 32(8):1028–1065, September 2022

work page 2022
[16]

M. J. Gabbay. Foundations of nominal techniques: Logic and semantics of variables in abstract syntax.Bulletin of Symbolic Logic, 17(2):161–229, 2011

work page 2011
[17]

K. Gödel. Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes. Dialectica, 12:280–287, 1958

work page 1958
[18]

Goguen, C

H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors,Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, pages 521–540. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006

work page 2006
[19]

A. D. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In J. J. Joyce and C.-J. H. Seger, editors,Higher Order Logic Theorem Proving and Its Applications, pages 413–425, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. ISBN 978-3-540- 48346-5

work page 1994
[20]

Harper.Practical Foundation for Programming Languages, Second Edition

R. Harper.Practical Foundation for Programming Languages, Second Edition. Cambridge University Press, 2016

work page 2016
[21]

M. Hedberg. A coherence theorem for Martin-Löf’s type theory.Journal of Functional Programming, 8(4):413–436, 1998

work page 1998
[22]

Martin-Löf

P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors,Logic Colloquium ’73, pages 73–118. North-Holland, 1975

work page 1975
[23]

Milner, J

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (parts I and II).Infor- mation and Computation, 100:1–77, 1992

work page 1992
[24]

Nipkow, L

T. Nipkow, L. C. Paulson, and M. Wenzel.Isabelle/HOL, A Proof Assistant for Higher-Order Logic, volume 2283 ofLecture Notes in Computer Science. Springer-Verlag, 2002

work page 2002
[25]

Nordström, K

B. Nordström, K. Petersson, and J. M. Smith.Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. 19

work page 1990
[26]

A. M. Pitts. Alpha-structural recursion and induction.Journal of the ACM, 53:459–506, 2006

work page 2006
[27]

A. M. Pitts.Nominal Sets: Names and Symmetry in Computer Science, volume 57 ofCam- bridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013

work page 2013
[28]

A. M. Pitts. Locally nameless sets.Proc. ACM Program. Lang., 7(POPL, Article 17):488–514, January 2023

work page 2023
[29]

Well-Scoped Locally Nameless Representation of Syntax

A. M. Pitts. Agda code accompanying “Well-Scoped Locally Nameless Representation of Syntax”, 2026. Browsable code:https://amp12.github.io/WSLN

work page 2026
[30]

G. D. Plotkin. An illative theory of relations. In R. Cooper, Mukai, and J. Perry, editors, Situation Theory and its Applications, Volume 1, volume 22 ofCSLI Lecture Notes, pages 133–146. Stanford University, 1990

work page 1990
[31]

A. Popescu. Rensets and renaming-based recursion for syntax with bindings. In J. Blanchette, L. Kovács, and D. Pattinson, editors,Automated Reasoning : 11th Interna- tional Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 ofLecture Notes in Computer Science, pages 618–639. Springer International Publish- ing AG, Au...

work page 2022
[32]

Sewell, F

P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strniša. Ott: Effective tool support for the working semanticist.Journal of Functional Programming, 20 (1):71–122, 2010

work page 2010
[33]

Stoughton

A. Stoughton. Substitution revisited.Theoretical Computer Science, 59:317–325, 1988

work page 1988
[34]

W. W. Tait. Intensional interpretation of functionals of finite type, I.Journal of Symbolic Logic, 32(2):198–212, 1967

work page 1967
[35]

Agda, version 2.8.0, July 2025

The Agda Development Team. Agda, version 2.8.0, July 2025. URLhttps://agda. readthedocs.io/en/stable

work page 2025
[36]

The Rocq prover, version 9.0, March 2025

The Rocq Development Team. The Rocq prover, version 9.0, March 2025. URLhttps: //rocq-prover.org

work page 2025
[37]

The Univalent Foundations Program.Homotopy Type Theory: Univalent Foundations for Mathematics.http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. 20

work page 2013