The presheaf model of abstract syntax and variable binding

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

• Dima Szamozvancev (University of Cambridge)
• Friday 29 January 2021, 11:00-12:00
• https://meet.google.com/jxy-edcv-wgx.

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.

This talk is included in these lists:

• Logic & Semantics for Dummies
• https://meet.google.com/jxy-edcv-wgx
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.