Verifying the Smallest Interesting Colour Code with Quantomatic
arXiv:1706.02717 · doi:10.4204/EPTCS.266.10
Abstract
In this paper we present a Quantomatic case study, verifying the basic properties of the Smallest Interesting Colour Code error detecting code.
arXiv commentIn Proceedings QPL 2017, arXiv:1802.09737. v2 removes the long appendix with the complete proofs. This is still available in v1 of this paper
References in corpus (17)
- Elementary gates for quantum computation
- Universal Quantum Computation with ideal Clifford gates and noisy ancillas
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- A Software Methodology for Compiling Quantum Programs
- Quantum computation with realistic magic state factories
- The ZX-calculus is complete for stabilizer quantum mechanics
- A unified framework for magic state distillation and multi-qubit gate-synthesis with reduced resource cost
- Unifying gate-synthesis and magic state distillation
- Pivoting makes the ZX-calculus complete for real stabilizers
- Verifying the Steane code with Quantomatic
- The ZX-calculus is complete for the single-qubit Clifford+T group
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- Making the stabilizer ZX-calculus complete for scalars
- A Simplified Stabilizer ZX-calculus
- Pattern graph rewrite systems
- Supplementarity is Necessary for Quantum Diagram Reasoning
- Tensors, !-graphs, and non-commutative quantum structures
Cited by in corpus (10)
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- Reconstructing quantum theory from diagrammatic postulates
- Optimising Clifford Circuits with Quantomatic
- ZX-calculus for the working quantum computer scientist
- Graphical Structures for Design and Verification of Quantum Error Correction
- Completeness of the ZX-Calculus
- SZX-calculus: Scalable Graphical Quantum Reasoning
- Optimizing ZX-Diagrams with Deep Reinforcement Learning
- The Qupit Stabiliser ZX-travaganza: Simplified Axioms, Normal Forms and Graph-Theoretic Simplification
- Transversal AND in Quantum Codes