Gottesman Types for Quantum Programs

TL;DR

This paper presents a type system based on Gottesman's semantics for analyzing quantum programs, extending the efficient simulation techniques beyond Clifford circuits to a broader class of quantum algorithms.

Contribution

It introduces a novel type-theoretic framework for quantum program analysis, expanding Gottesman's approach to non-Clifford circuits for better reasoning about quantum states and algorithms.

Findings

Efficiently characterizes a subset of quantum programs using types.

Extends Gottesman's semantics beyond Clifford circuits.

Applies types to analyze superdense coding and separable states.

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.