About

*** This is the old Quantomatic website. The new page is at ***



Overview

Open graph based formalisms give an abstract and symbolic way to describe computation. In particular, quantum information processing has a beautiful graphical description. However, manual manipulation of such graphs is slow and error prone. This project uses a graphical language, based on monoidal categories, to support mechanised reasoning with open-graphs. In particular, Quantomatic's graph rewriting preserves the underlying categorical semantics.

We are using open graphs as the representation for a generic 'logical' system (with a fixed logical-kernel) that supports reasoning about models of compact closed category. This 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, hence the name 'Quantomatic'.

See Publications and more discussion and details, and ask questions on the Quantomatic Google Group.

The System and its Installation

We have an implementation built using libraries from Isabelle and IsaPlanner. This builds on Poly/ML, Java, and Graphviz. See Getting Started for details on how to get hold of Quantomatic.

People and Organisations

  • Aleks Kissinger - Department of Computer Science, University of Oxford
  • Alex Merry - Department of Computer Science, University of Oxford
  • Ben Frot - Department of Computer Science, University of Oxford
  • Bob Coecke - Department of Computer Science, University of Oxford
  • David Quick - Department of Computer Science, University of Oxford
  • Lucas Dixon - Informatics, University of Edinburgh and Google
  • Matvey Soloviev - University of Cambridge
  • Ross Duncan - Laboratoire d'Information Quantique, Université Libre de Bruxelles
  • Vladimir Zamdzhiev - Department of Computer Science, University of Oxford

Other Links

Support

This work is funded by:

EPSRC FQXi
ONR QICS