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 and Semantics Seminar (Computer Laboratory)
SUMMARY:Coherent differentiation makes the differential la
mbda-calculus deterministic - Thomas Ehrhard\, Uni
versity of Paris
DTSTART;TZID=Europe/London:20221028T140000
DTEND;TZID=Europe/London:20221028T150000
UID:TALK184934AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/184934
DESCRIPTION:Categorical models of differentiation are either a
dditive categories\,\nthat is categories enriched
over commutative monoids\, or left-additive\ncateg
ories. This is due to the fact that the differenti
ation of a\nfunction depending on a tuple of argum
ents requires a summation of\npartial derivatives.
From a computational point of view this means tha
t\na model of a programming language where program
s can be differentiated\n(in the sense of the diff
erential lambda-calculus) features a strong\nform
of non-determinism. The recently introduced cohere
nt\ndifferentiation shows that this is not a fatal
ity\, proposing a new\nsetting where morphisms can
be differentiated - in a completely standard\nway
- in categories which are not necessarily additiv
e. As an outcome we\nintroduce a differential vers
ion of the functional language PCF equipped\nwith
a fully deterministic operational semantics. This
new approach is\nbased on a functorial axiomatizat
ion of the concept of summability.
LOCATION:SS03
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR