Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Aarthi Sundaram, Robert Rand, Kartik Singhal +2

We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a…