111 citations · 347 across the 14 of their papers we have counts for
4 papers · 1 filter
A Verified Optimizer for Quantum Circuits
Kesha Hietala, Robert Rand, Shih-Han Hung +2
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level l…
Verification Logics for Quantum Programs
Robert Rand
We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for for…
Verified Optimization in a Quantum Intermediate Representation
Kesha Hietala, Robert Rand, Shih-Han Hung +2
We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum…
ReQWIRE: Reasoning about Reversible Quantum Circuits
Robert Rand, Jennifer Paykin, Dong-Ho Lee +1
Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit lan…