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:Higher Algebra in Computer Science - Eric Finster\
, University of Cambridge
DTSTART;TZID=Europe/London:20201009T140000
DTEND;TZID=Europe/London:20201009T150000
UID:TALK152572AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/152572
DESCRIPTION:https://youtu.be/pD8M4u30dHM\n\nThe field of highe
r dimensional algebra can be described as the exte
nsion of ordinary algebra to situations which are
"proof relevant"\, which is to say\, in which equa
tions must themselves be regarded as structure and
not merely properties of the underlying data. Pe
rhaps the most well-known examples of this phenome
non arise from attempts at extending the notion of
category to higher dimensions\, a subject known g
enerally as higher category theory. But many othe
r examples are known from topology\, and recent de
velopments linking dependent type theory and homot
opy theory have shown the relevance of these for f
ormal proof assistants. In this talk\, I will sur
vey some of the ideas arising from this point of v
iew and detail their applications in computer scie
nce. Time permitting\, I will describe a small ty
pe theory called Catt which illustrates some of th
e main principles of the higher algebraic approach
.
LOCATION:Online
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR