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.

Selected Publications

View All

• 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 about Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation | BibTeX data for Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation | Download of Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation | DOI (10.1007/978-3-540-85110-3_8)

• 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 about Interacting Quantum Observables | BibTeX data for Interacting Quantum Observables | Download  (pdf) of Interacting Quantum Observables | DOI (10.1007/978-3-540-70583-3_25)

• Graphical Reasoning in Compact Closed Categories for Quantum Computation

  Lucas Dixon and Ross Duncan

  In Annals of Mathematics and Artificial Intelligence. 2009.

  preprint available at http://arxiv.org/abs/0902.0514

  Details about Graphical Reasoning in Compact Closed Categories for Quantum Computation | BibTeX data for Graphical Reasoning in Compact Closed Categories for Quantum Computation | Download  (pdf) of Graphical Reasoning in Compact Closed Categories for Quantum Computation | DOI (10.1007/s10472-009-9141-x)