Gottesman Types for Quantum Programs

Robert Rand
(University of Chicago)
Aarthi Sundaram
(Microsoft Quantum)
Kartik Singhal
(University of Chicago)
Brad Lackey
(Microsoft Quantum and University of Maryland)

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.

In Benoît Valiron, Shane Mansfield, Pablo Arrighi and Prakash Panangaden: Proceedings 17th International Conference on Quantum Physics and Logic (QPL 2020), Paris, France, June 2 - 6, 2020, Electronic Proceedings in Theoretical Computer Science 340, pp. 279–290.
Published: 6th September 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: