Formal Metatheory of Second-Order Abstract Syntax

Marcelo Fiore, Dmitrij Szamozvancev


  1. If building from source, clone the Git repository (and submodules) with git clone --recurse-submodules
  2. If using VirtualBox:
    1. Download the virtual machine and double-click on the downloaded SOAS.ova file (or File > Import Appliance... in VirtualBox).
    2. Launch the virtual machine with VirtualBox and log in with username agda-soas and password popl2022-agda-soas. You may need to resize the window or tweak the Display settings in VirtualBox to adjust scaling.
    3. Open Emacs and navigate to the ~/agda-soas directory (or navigate to ~/agda-soas in the Terminal and open Emacs with emacs .)
  3. Open any of the code files in the SOAS directory (the modules are listed in Everything.agda) and load it with C-c C-l. Same for example files, found in the subfolders of the out directory.
  4. Call the code generation script with python3 <filename>, with some examples given in the gen/ex directory.

Correspondence guide

Much of the code in the library is directly included in the paper. Below is a section-by-section listing of the defined concepts and their location in the source code.

The formalisation depends on the Agda standard library and category theory library, and uses implicit and explicit function extensionality (and some derived properties for convenience). The REWRITE pragma is used for some nonessential proofs that are not required for the main results.

2. Mathematical foundations

Formalisation of abstract mathematical concepts used in the library, including the standard inductive definition of contexts and variables (typed de Bruijn indices), type- and context-indexed families of sets, the axiomatisation of renaming and substitution structure, and properties of functions that incorporate a substitution.

2.1. Contexts and families

2.2. Renaming and substitution

2.3. Parametrised maps

3. Initial algebra semantics

The initial algebra semantics approach underlies most of the metatheoretic results. The signature-generic development is accomplished by parametrising the relevant modules with a metavariable family and a signature endofunctor with a coalgebraic strength, and furthermore assuming the existence of an initial meta-algebra for the endofunctor from which initial interpretations can be extracted. Specifically, initiality states that given any meta-algebra 𝒜, there exists a unique meta-algebra homomorphism 𝕤𝕖𝕞 : 𝕋 ⇾ 𝒜 where 𝕋 is the initial meta-algebra assumed to exist.

3.1. Signature algebras and monoids

3.3. Parametrised interpretations

3.4. ⅀-monoid structure by initiality

3.5. Free ⅀-monoid structure

3.6-7. Metasubstitution and equational systems

4. Generic signatures

The signature endofunctor forms the brigde between a second-order signature and the generic metatheory. Initial algebras for the endofunctor (i.e. algebraic data types whose constructors form term of the syntax) can be defined in several ways: either by directly using the signature endofunctor and combining every operator into a single constructor, or separating the operators into individual constructors. The latter is more convenient in practice, and there is a Python script that generates the required boilerplate automatically.

4.1-2. Binding signatures and endofunctor

4.3. Term syntax

4.4. Code generation