BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The presheaf model of abstract syntax and variable binding - Dima 
 Szamozvancev (University of Cambridge)
DTSTART:20210129T110000Z
DTEND:20210129T120000Z
UID:TALK156838@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:On Page 26 of his 600-page epic ‘The Lambda Calculus: Its Sy
 ntax and Semantics’\, Henk Barendregt introduced the Variable Convention
 : if several language terms appear in a mathematical context\, then in the
 se terms all bound variables are chosen to be different from the free vari
 ables. 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 formal
 ise a language knows that dealing with variable binding and substitution i
 s error-prone and very finicky\, often requiring long series of auxiliary 
 definitions and ad-hoc lemmas just to get single-variable substitution wor
 king.\n\nThe nuanced nature of the problem is further evidenced by the dec
 ades 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 o
 f formal systems\, and extended to support second-order equational reasoni
 ng and algebraic theories. This talk will introduce the main components of
  the categorical theory – presheaves\, initial algebra semantics\, the s
 ubstitution monoidal structure – and potentially touch upon its develop
 ment into a language formalisation framework in Agda.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR