University of Edinburgh
4pm Tuesday, 16th February, 2010
Room 4.31/33, Informatics Forum
Symmetric monoidal categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. I will present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel. A salient feature of our system is that it provides a formal and declarative account of derived results that can include 'ellipses'-style notation. I will illustrate the framework by describing the graphical language applied to quantum computation and boolean circuits, and briefly show how this can be used to perform computations symbolically.