@inproceedings{Dixon:2008ys,
  abstract = "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. We present 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 describe 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. We illustrate the framework by instantiating it for a graphical language of quantum computation and show how this can be used to perform symbolic computation.",
  author = "Lucas Dixon and Ross Duncan",
  booktitle = "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",
  doi = "10.1007/978-3-540-85110-3_8",
  editor = "Autexier, Serge and Campbell, John and Rubio, Julio and Sorge, Volker and Suzuki, Masakazu and Wiedijk, Freek",
  keywords = "rewriting; quantum computing; categorical logic; interactive theorem proving; graphical calculi",
  pages = "77-92",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  title = "Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation",
  volume = "5144",
  year = "2008",
}