1

Gottesman Types for Quantum Programs
Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey
PDF Cite Slides Video
Formal Verification vs. Quantum Uncertainty
Robert Rand, Kesha Hietala, Michael Hicks
PDF Cite Slides
ReQWIRE: Reasoning about Reversible Quantum Circuits
Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic
PDF Cite Code Slides Video DOI
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
Robert Rand, Jennifer Paykin, Steve Zdancewic
PDF Cite Code Slides DOI
QWIRE: A Core Language for Quantum Circuits

This paper introduces QWIRE ("choir"), a language for defining quantum circuits and an interface for manipulating them inside of an …
Jennifer Paykin, Robert Rand, Steve Zdancewic
PDF Cite Code Slides DOI
VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs
We introduce a Hoare-style logic for probabilistic programs, called VPHL, that has been formally verified in the Coq proof assistant. …
Robert Rand, Steve Zdancewic
PDF Cite Slides DOI