University of Cambridge > > Logic & Semantics for Dummies > The presheaf model of abstract syntax and variable binding

The presheaf model of abstract syntax and variable binding

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Nathanael Arkor.

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.

This talk is part of the Logic & Semantics for Dummies series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity