University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Oxford Quantum Talks Archive

String diagrams, a topological account of proofs and programs

Paul-Andre Mellies, Laboratoire PPS, Paris VIII
Seminars, February 2010, University of Oxford

In this introductory talk, I will explain some of the functorial ideas which recently appeared in the field of logic and programming language semantics. More specifically, I will explain how to see game semantics as a variant of functorial knot theory, where the ribbon category of knots is replaced by a monoidal category of formulas and proofs between them. By the wizardry of string diagrams in 3-categories, this category may be seen alternatively as a category of games and interactive strategies between them. Interestingly, this game construction defines the free symmetric monoidal category equipped with a logical duality. From this follows the idea of classifying the various notions of duality in monoidal categories, the usual duality of ribbon categories being one of them. For the fun of it, I will also describe how to compute the free monoid in that category of games, using a left Kan extension, and relate this construction to the ability to define recursive calls in programming languages. Finally, I will draw a beautiful connection between logic and algebra, first noticed by Ross Street, and explain in what sense this category of games may be seen as a lax notion of Frobenius algebra. Amusingly, this observation leads to a lax version of two-dimensional cobordism, where particles are replaced by game boards.

[video] [streaming video]