Static Analysis of Quantum Programs via Gottesman Types
Abstract
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (nonuniversal) Clifford set $H$, $S$ and $CNOT$. The GottesmanKnill 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 apply this primarily towards tracking entanglement in programs, showing how superdense coding and GHZ circuits entangle and disentangle qubits and how to safely dispose of ancillae. We demonstrate the efficiency of our typechecking algorithm both for simple deductions and those involving entanglement and measurement.
 Publication:

arXiv eprints
 Pub Date:
 January 2021
 arXiv:
 arXiv:2101.08939
 Bibcode:
 2021arXiv210108939R
 Keywords:

 Quantum Physics;
 Computer Science  Emerging Technologies;
 Computer Science  Logic in Computer Science;
 Computer Science  Programming Languages;
 F.3.1;
 D.2.4;
 F.4.1;
 I.1.1
 EPrint:
 18 pages, 3 figures