BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:The presheaf model of abstract syntax and variable
binding - Dima Szamozvancev (University of Cambri
dge)
DTSTART;TZID=Europe/London:20210129T110000
DTEND;TZID=Europe/London:20210129T120000
UID:TALK156838AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/156838
DESCRIPTION:On Page 26 of his 600-page epic ‘The Lambda Calcul
us: Its Syntax and Semantics’\, Henk Barendregt in
troduced the Variable Convention: if several langu
age terms appear in a mathematical context\, then
in these terms all bound variables are chosen to b
e different from the free variables. Though it’s a
n innocent-looking and easily fulfilled condition\
, its widespread use in pen-and-paper research may
erroneously suggest that the issues of variable n
ames\, alpha-conversion and capture avoidance can
be swept under the carpet. Anyone who’s attempted
to implement or formalise a language knows that de
aling with variable binding and substitution is er
ror-prone and very finicky\, often requiring long
series of auxiliary definitions and ad-hoc lemmas
just to get single-variable substitution working.\
n\nThe nuanced nature of the problem is further ev
idenced by the decades of research trying to place
abstract syntax with variable binding on a formal
\, mathematical foundation. One such attempt is th
e presheaf model of Fiore et al.\, which has been
successfully adapted to varied notions of formal s
ystems\, and extended to support second-order equa
tional reasoning and algebraic theories. This talk
will introduce the main components of the categor
ical theory – presheaves\, initial algebra semanti
cs\, the substitution monoidal structure – and pot
entially touch upon its development into a languag
e formalisation framework in Agda.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR