Formal Metatheory of Second-Order Abstract Syntax

TL;DR

This paper introduces a formal framework in Agda for defining and reasoning about languages with variable binding, leveraging initial algebra semantics to ensure correctness and support second-order reasoning.

Contribution

It presents a novel Agda-based formalisation that automatically encodes syntax with variable binding and supports second-order reasoning through metavariables and metasubstitution.

Findings

Automatically encodes syntax signatures with variable binding

Ensures correctness properties via inductive data types

Supports second-order equational and rewriting reasoning

Abstract

Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour - repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning. The underlying mathematical foundation of the framework - initial algebra semantics - derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.