BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Higher Algebra in Computer Science - Eric Finster\, University of 
 Cambridge
DTSTART:20201009T130000Z
DTEND:20201009T140000Z
UID:TALK152572@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:https://youtu.be/pD8M4u30dHM\n\nThe field of higher dimensiona
 l algebra can be described as the extension of ordinary algebra to situati
 ons which are "proof relevant"\, which is to say\, in which equations must
  themselves be regarded as structure and not merely properties of the unde
 rlying data.  Perhaps the most well-known examples of this phenomenon aris
 e from attempts at extending the notion of category to higher dimensions\,
  a subject known generally as higher category theory.  But many other exam
 ples are known from topology\, and recent developments linking dependent t
 ype theory and homotopy theory have shown the relevance of these for forma
 l proof assistants.  In this talk\, I will survey some of the ideas arisin
 g from this point of view and detail their applications in computer scienc
 e.  Time permitting\, I will describe a small type theory called Catt whic
 h illustrates some of the main principles of the higher algebraic approach
 .
LOCATION:Online
END:VEVENT
END:VCALENDAR