BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Formalizing compositional proofs - Jamie Vicary (U
niversity of Oxford)
DTSTART:20161014T100000Z
DTEND:20161014T110000Z
UID:TALK2195AT
URL:/talk/index/2195
DESCRIPTION:I will present a new proof assistant\, Globular\,
which allows the formalization of compositional pr
oofs in higher category theory. The interface is g
eometrical\, with proofs depicted as string diagra
ms\, and allowing direct click-and-drag manipulati
on. I will show how to build a simple proof from s
cratch\, and present some sophisticated formalized
proofs from topology and algebra. I will also giv
e some details of the theoretical basis. This talk
will be accessible\, and will not require any pre
vious knowledge of category theory.\n
LOCATION:Computer Science\, The Sloman Lounge (UG)
CONTACT:Paul Taylor
END:VEVENT
END:VCALENDAR