Abstract

On Page 26 of his 600-page epic ‘The Lambda Calculus: Its Syntax and Semantics’, Henk Barendregt introduced the Variable Convention: if several language terms appear in a mathematical context, then in these terms all bound variables are chosen to be different from the free variables. Though it’s an innocent-looking and easily fulfilled condition, its widespread use in pen-and-paper research may erroneously suggest that the issues of variable names, alpha-conversion and capture avoidance can be swept under the carpet. Anyone who’s attempted to implement or formalise a language knows that dealing with variable binding and substitution is error-prone and very finicky, often requiring long series of auxiliary definitions and ad-hoc lemmas just to get single-variable substitution working.

The nuanced nature of the problem is further evidenced by the decades of research trying to place abstract syntax with variable binding on a formal, mathematical foundation. One such attempt is the presheaf model of Fiore et al., which has been successfully adapted to varied notions of formal systems, and extended to support second-order equational reasoning and algebraic theories. This talk will introduce the main components of the categorical theory – presheaves, initial algebra semantics, the substitution monoidal structure – and potentially touch upon its development into a language formalisation framework in Agda.