Overview
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
- Ross Duncan, Simon Perdrix. Rewriting Measurement-Based Quantum Computations with Generalised Flow., ICALP
2010 [12 pages, springer]
- Lucas Dixon, Ross Duncan, A. Kissinger. Open Graphs and Computational Reasoning, DCM
2010 [12 pages, pdf]
- Bob Coecke and Aleks Kissinger. The compositional structure of multipartite quantum entanglement, ICALP 2010. [arxiv paper]
- Ross Duncan and Simon Perdrix. Graph States and the necessity of Euler Decomposition, Computability in Europe: Mathematical Theory and Computational Practice (CiE'09). [arxiv paper]
- Lucas Dixon and Aleks Kissinger. Monoidal Categories, Graphical
Reasoning, and Quantum Computation, Extended Abstract
[14 pages,
2009, pdf].
- Lucas Dixon and Ross Duncan. Graphical Reasoning in
Compact Closed Categories for Quantum Computation, AMAI, special issue on AISC 2008 [20 pages, 2008, pdf, Springer].
- Bob Coecke and Ross Duncan. Interacting Quantum Observables, ICALP 2008, [arxiv paper]
- Aleks Kissinger. Exploring a Quantum Theory with Graph Rewriting and Computer Algebra, LNCS proceedings of Calculemus 2009 [15 pages, 2009, pdf].
- Lucas Dixon and Ross Duncan. Extending Graphical Representations
for Compact Closed Categories with Applications to Symbolic Quantum
Computation, AISC 2008 [16 pages, 2008 pdf]. (Note the
journal article in AMAI, above, makes significant improvements on this
paper - read that instead)
Posters
- Lucas Dixon and Ross Duncan and Aleks Kissinger, Graph Rewriting for Classical Structures, Poster Presented at QICS 2008 [A0 poster, 2008, pdf].
Talks
- Introduction and demo of Quantomatic (20 minute Oxford computing lab video), presented by Lucas Dixon at the QICS Summer School (see also the other videos from QICS) held at the University of Oxford, May 2010.
- Graphical Reasoning in Symmetric Monoidal Categories for
Quantum Information. Lucas Dixon.
[slides as pdf, 1hr
with demo] Invited talk
for The
Wednesday Seminar, University of Cambridge, 27 Jan 2010.
- Graphical reasoning in symmetric monoidal categories. Lucas Dixon. Invited talk at University of Leicester, 5 Nov 2009 [pdf]
- Monoidal Theories and Graph Rewriting in Quantum Computing. Aleks Kissenger and Lucas Dixon. At CAM-CAD, 17 Oct 2009 [pdf]
- Quantum CS with Graph Rewriting and CAS. Aleks Kissenger. Calculemus, 6 Jul 2009 [pdf]
