Quantomatic: Automated Reasoning with Open Graphs
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.
See the Quantomatic website for more information.
People
|
Contact for Activity |
|
|
Faculty |
|
|
Research |
|
|
Students |
|
|
Past Members |
|
Selected Publications
| Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation Lucas Dixon and Ross Duncan In Serge Autexier‚ John Campbell‚ Julio Rubio‚ Volker Sorge‚ Masakazu Suzuki and Freek Wiedijk, editors, Intelligent Computer Mathematics‚ 9th International Conference‚ AISC 2008‚ 15th Symposium‚ Calculemus 2008‚ 7th International Conference‚ MKM 2008‚ Birmingham‚ UK‚ July 28 − August 1‚ 2008. Proceedings. Vol. 5144 of Lecture Notes in Computer Science. Pages 77−92. Springer. 2008. Details | BibTeX | Download | DOI (10.1007/978-3-540-85110-3_8) |
| Exploring a Quantum Theory with Graph Rewriting and Computer Algebra Aleks Kissinger 2009. |
| Interacting Quantum Observables Bob Coecke and Ross Duncan In Automata‚ Languages and Programming‚ 35th International Colloquium‚ ICALP 2008‚ Reykjavik‚ Iceland‚ July 7−11‚ 2008‚ Proceedings‚ Part II. Vol. 5126 of Lecture Notes in Computer Science. Pages 298−310. Springer. 2008. A significantly revised and expanded version of this paper is available as preprint http://arxiv.org/abs/0906.4725 Details | BibTeX | Download (pdf) | DOI (10.1007/978-3-540-70583-3_25) |
Links
Quantomatic homepage
Subversion repository
Issue tracker
Info
|
Themes |
Funding
|
