Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Abstract

We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate.

52 pages, 3 figures

References in corpus (15)

• Improved Simulation of Stabilizer Circuits
• Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
• Fault-tolerant conversion between the Steane and Reed-Muller quantum codes
• Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs
• A Deductive Verification Framework for Circuit-building Quantum Programs
• Quantum entanglement analysis based on abstract interpretation
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• A logical analysis of entanglement and separability in quantum higher-order functions
• Efficient Formal Verification of Quantum Error Correcting Programs
• Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism
• Gottesman Types for Quantum Programs
• Programming with union, intersection, and negation types
• A Practical Quantum Hoare Logic with Classical Variables, I