MRG home page · Research · Publications · Projects · Software · People



Recent graph-based formalisms of quantum computation provide an abstract and symbolic way to represent and simulate computations. However, manual manipulation of such graphs is slow and error prone. This project employs a formalism, based on compact closed categories, that supports mechanised reasoning about such graphs. This gives a compositional account of graph rewriting that preserves the underlying categorical semantics.

Using this representation, we are developing a generic system with a fixed logical kernel that supports reasoning about models of compact closed category. A salient feature of the system is that it provides a formal and declarative account of derived results that can include ellipses-style notation. The main application is to develop a graph-based language for reasoning about quantum computation: Quantomatic.

The Quantomatic homepage has moved to the Quantomatic Google site; you can find the latest information on how to download and install the system, as well as a more recent list of papers there.

Related Publications from when this project was actively worked on in Edinburgh



Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the Lucas Dixon
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.