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 InstallationWe 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
|
