Warning - the bibtex entry below may be invalid: Missing 'chapter' or 'pages' field @inbook{Duncan:2009cs, abstract = "Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.", author = "Ross Duncan", booktitle = "Semantics of Quantum Computation", editor = "S. Gay and I. Mackie", keywords = "categorical quantum mechanics; compact closed categories; proof-nets; quantum computing", note = "Preprint available at http://arxiv.org/abs/0903.5154", publisher = "Cambridge University Press", title = "Generalised Proof-Nets for Compact Categories with Biproducts", year = "2009", } @inproceedings{Duncan:2009ph, abstract = "Coecke and Duncan recently introduced a categorical formalisation of the interaction of complementary quantum observables. In this paper we use their diagrammatic language to study graph states, a computationally interesting class of quantum states. We give a graphical proof of the fixpoint property of graph states. We then introduce a new equation, for the Euler decomposition of the Hadamard gate, and demonstrate that Van den Nest's theorem--locally equivalent graphs represent the same entanglement--is equivalent to this new axiom. Finally we prove that the Euler decomposition equation is not derivable from the existing axioms.", author = "Ross Duncan and Simon Perdrix", booktitle = "Computability in Europe: Mathematical Theory and Computational Practice (CiE'09)", doi = "10.1007/978-3-642-03073-4", editor = "Ambos-Spies, K. and L\"{o}we, B. and Merkle, W.", keywords = "quantum computing; categorical quantum mechanics; graphical calculi; measurement-based quantum computing; entanglement", note = "Preprint available at http://arxiv.org/abs/0902.0500", pages = "167--177", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Graph States and the necessity of Euler Decomposition", volume = "5635", year = "2009", } @article{Lucas-Dixon:2009yq, abstract = "Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our 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", doi = "10.1007/s10472-009-9141-x", journal = "Annals of Mathematics and Artificial Intelligence", keywords = "categorical quantum mechanics; compact closed categories; rewriting; graphical calculi", note = "preprint available at http://arxiv.org/abs/0902.0514", title = "Graphical Reasoning in Compact Closed Categories for Quantum Computation", year = "2009", } @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", } @inproceedings{Coecke:2008nx, abstract = "We formalise the constructive content of an essential feature of quantum mechanics: the interaction of complementary quantum observables, and information flow mediated by them. Using a general categorical formulation, we show that pairs of mutually unbiased quantum observables form bialgebra-like structures. We also provide an abstract account on the quantum data encoded in complex phases, and prove a normal form theorem for it. Together these enable us to describe all observables of finite dimensional Hilbert space quantum mechanics. The resulting equations suffice to perform computations with elementary quantum gates, translate between distinct quantum computational models, establish the equivalence of entangled quantum states, and simulate quantum algorithms such as the quantum Fourier transform. All these computations moreover happen within an intuitive diagrammatic calculus.", author = "Bob Coecke and Ross Duncan", booktitle = "Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II", doi = "10.1007/978-3-540-70583-3_25", keywords = "categorical quantum mechanics; quantum computing;", note = "A significantly revised and expanded version of this paper is available as preprint http://arxiv.org/abs/0906.4725", pages = "298-310", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Interacting Quantum Observables", volume = "5126", year = "2008", } Warning - the bibtex entry below may be invalid: Missing 'school' field @phdthesis{Duncan:thesis:2006, author = "Ross Duncan", institution = "Oxford University", note = "This thesis was the runner up for the British Computer Society Distinguished Dissertation award.", title = "Types for Quantum Computing", url = "http://www.bcs.org/server.php?show=conMediaFile.10119", year = "2006", } @article{AbrDun:CQLv2:2004, abstract = "We define a strongly normalising proof-net calculus corresponding to the logic of strongly compact closed categories with biproducts. The calculus is a full and faithful representation of the free strongly compact closed category with biproducts on a given category with an involution. This syntax can be used to represent and reason about quantum processes.", author = "Samson Abramsky and Ross Duncan", doi = "10.1017/S0960129506005275", journal = "Mathematical Structures in Computer Science", note = "Preprint available at http://arxiv.org/abs/quant-ph/0512114", number = "3", pages = "469-489", title = "A Categorical Quantum Logic", volume = "16", year = "2006", } @inproceedings{AbrDun:CQLv1:2004, abstract = "We define a sequent calculus corresponding to the logic of strongly compact closed categories with biproducts. Based on this calculus, we define a proof-net syntax with a strongly normalising cut-elimination. This syntax encodes abstract qualitative and quantitative information about the behaviour of quantum processes.", author = "Samson Abramsky and Ross Duncan", booktitle = "Proceedings of the 2nd International Workshop on Quantum Programming Languages", edition = "Selinger, Peter", keywords = "quantum computing; compact closed categories; proof-nets", note = "This paper is largely superceded by the MSCS publication with the same title, however some details, such as the sequent calculus presentation, are only found in this version.", series = "Turku Centre for Computer Science General Publication", title = "A Categorical Quantum Logic", url = "http://quasar.mathstat.uottawa.ca/~selinger/qpl2004/PDFS/02Abramsky-Duncan.pdf", volume = "33", year = "2004", } @techreport{RR-04-18, author = "Ross Duncan", institution = "Oxford University Computing Laboratory", month = "October", number = "RR-04-18", title = "Believe it or not, Bell states are a model of multiplicative linear logic", year = "2004", }