adgda/WSLN is an Agda library for the well-scoped version of the locally nameless method of representing syntax. The library is parameterised by a Plotkin-style binding signature and makes use of some (more or less) standard library definitions in agda/Prelude.
agda/Adequacy gives a proof of the adequacy of this style of representation with respect to naïve nameful syntax modulo α-conversion
Checked with Agda version 2.8.0 using flags
--safe
--without-K
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.
Examples of binding signatures: untyped λ-calculus, π-calculus
Martin-Löf Type Theory with countably many Agda-style non-cumulative universes closed under Pi-types, natural number type and intensional identity types.
Gödel’s System T. Decidability of βη-conversion using well-scoped locally nameless syntax, proved via a normalization by evaluation argument, in safe Agda.