  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.
