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:New reasoning techniques for monoidal algebras - A
leks Kissinger\, University of Oxford
DTSTART;TZID=Europe/London:20150116T160000
DTEND;TZID=Europe/London:20150116T170000
UID:TALK55913AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/55913
DESCRIPTION:In this talk\, I will discuss the interaction of t
wo prominent tools\none uses to study algebraic st
ructures in monoidal categories: PROPs\nand string
diagram rewriting. PROPs are small symmetric mono
idal\ncategories which totally capture a certain a
lgebraic structure (they\nare the "walking X")\, b
ut their application is typically limited to\nstru
ctures that we understand well. On the other hand\
, rewriting with\nstring diagrams allows one to im
mediately get a handle on even those\nstructures w
hich have very complicated presentations\, but it
provides\nlittle in the way of powerful "meta-rule
s" describing the global\nbehaviour of the structu
re.\n\nTo bridge this gap\, one needs to find more
sophisticated ways of\nexpressing and reasoning a
bout infinite families of diagrams. In this\ntalk\
, I will introduce "!-box notation"\, which gives
a particularly\nsimple means of doing just that. W
hile the expressive power of !-boxes\nis fairly li
mited\, when combined with the notions of !-graph
rewriting\nand induction\, one can state and prove
a surprisingly rich family of\ntheorems\, and som
etimes even recapture the kind of global behaviour
we\nwould expect from a PROP-based approach. I wi
ll illustrate this by\ngiving a purely graphical p
roof of a recent representation theorem for\ninter
acting bialgebras\, and show this theorem in actio
n in the\ngraphical proof assistant Quantomatic.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Jonathan Hayman
END:VEVENT
END:VCALENDAR