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.

翻译：量子操作员的海森堡代表为量子电路的推理提供了强有力的技巧,尽管这些推理仅限于普通(非普遍)克里夫德设置的H、S和CNOT。高特斯曼-科尔理论显示,我们可以利用这种推理来高效模拟克里福德电路。我们显示,高特斯曼用于量子程序的语义可以被当作一种类型系统,从而使我们能够有效地描述量子程序的一个共同子集。我们还表明,它可以超越克利福德设定的范围,部分地描述范围广泛的程序。我们将这些推算用于解释可分离的状态和超常编码算法。