BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:New reasoning techniques for monoidal algebras - Aleks Kissinger\,
  University of Oxford
DTSTART:20150116T160000Z
DTEND:20150116T170000Z
UID:TALK55913@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:In this talk\, I will discuss the interaction of two prominent
  tools\none uses to study algebraic structures in monoidal categories: PRO
 Ps\nand string diagram rewriting. PROPs are small symmetric monoidal\ncate
 gories which totally capture a certain algebraic structure (they\nare the 
 "walking X")\, but their application is typically limited to\nstructures t
 hat we understand well. On the other hand\, rewriting with\nstring diagram
 s allows one to immediately get a handle on even those\nstructures which h
 ave very complicated presentations\, but it provides\nlittle in the way of
  powerful "meta-rules" describing the global\nbehaviour of the structure.\
 n\nTo bridge this gap\, one needs to find more sophisticated ways of\nexpr
 essing and reasoning about infinite families of diagrams. In this\ntalk\, 
 I will introduce "!-box notation"\, which gives a particularly\nsimple mea
 ns of doing just that. While 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 s
 ometimes even recapture the kind of global behaviour we\nwould expect from
  a PROP-based approach. I will illustrate this by\ngiving a purely graphic
 al proof of a recent representation theorem for\ninteracting bialgebras\, 
 and show this theorem in action in the\ngraphical proof assistant Quantoma
 tic.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR