44 citations · 65 across the 5 of their papers we have counts for
5 papers · 1 filter
Gottesman Types for Quantum Programs
Robert Rand, Aarthi Sundaram, Kartik Singhal +1
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Cliffor…
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…
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
Robert Rand, Jennifer Paykin, Steve Zdancewic
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to pr…