Gottesman Types for Quantum Programs
arXiv:2109.02197 · doi:10.4204/EPTCS.340.14
Abstract
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set H, S and CNOT. The Gottesman-Knill theorem showed that we can use this representation to efficiently simulate Clifford circuits. We show that Gottesman's semantics for quantum programs can be treated as a type system, allowing us to efficiently characterize a common subset of quantum programs. We also show that it can be extended beyond the Clifford set to partially characterize a broad range of programs. We apply these types to reason about separable states and the superdense coding algorithm.
arXiv commentIn Proceedings QPL 2020, arXiv:2109.01534. arXiv admin note: substantial text overlap with arXiv:2101.08939
References in corpus (16)
- A Class of Quantum Error-Correcting Codes Saturating the Quantum Hamming Bound
- Quantum Computing with Very Noisy Devices
- Instantaneous non-local computation of low T-depth quantum circuits
- The Heisenberg Representation of Quantum Computers
- Active stabilisation, quantum computation and quantum state synthesis
- Universal fault-tolerant quantum computation with only transversal gates and error correction
- Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
- Efficient Computations of Encodings for Quantum Error Correction
- Entanglement in the stabilizer formalism
- GHZ extraction yield for multipartite stabilizer states
- Local unitary versus local Clifford equivalence of stabilizer states
- Quantum entanglement analysis based on abstract interpretation
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Rewiring Stabilizer Codes
- Universal fault-tolerant quantum computation with Bacon-Shor codes
- Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism