72 citations · 159 across the 11 of their papers we have counts for
12 papers
Staged Hybrid Quantum-Classical Programming
Chuta Sano, Peng Fu, Ryan Kavanagh +2
Hybrid quantum-classical computing systems consist of a classical control system that sends quantum circuits and receives measurement results from a quantum co-processor. Such syst…
Qoreo: Choreographic Programming for Quantum Distributed Systems
Jennifer Paykin, Steven Baldasty, Joseph P. Near +1
Programming distributed quantum systems requires multiple actors to coordinate precise sequences of quantum operations, classical communication, and entanglement generation. Writin…
Verifying Fault-Tolerance of Quantum Error Correction Codes
Kean Chen, Yuhao Liu, Wang Fang +5
Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC)…
PCOAST: A Pauli-based Quantum Circuit Optimization Framework
Jennifer Paykin, Albert T. Schmitz, Mohannad Ibrahim +2
This paper presents the Pauli-based Circuit Optimization, Analysis, and Synthesis Toolchain (PCOAST), a framework for quantum circuit optimizations based on the commutative propert…
Optimization at the Interface of Unitary and Non-unitary Quantum Operations in PCOAST
Albert T. Schmitz, Mohannad Ibrahim, Nicolas P. D. Sawaya +4
The Pauli-based Circuit Optimization, Analysis and Synthesis Toolchain (PCOAST) was recently introduced as a framework for optimizing quantum circuits. It converts a quantum circui…
Formal Verification of Flow Equivalence in Desynchronized Designs
Jennifer Paykin, Brian Huffman, Daniel M. Zimmerman +1
Seminal work by Cortadella, Kondratyev, Lavagno, and Sotiriou includes a hand-written proof that a particular handshaking protocol preserves flow equivalence, a notion of equivalen…
Weird Machines as Insecure Compilation
Jennifer Paykin, Eric Mertens, Mark Tullsen +4
Weird machines---the computational models accessible by exploiting security vulnerabilities---arise from the difference between the model a programmer has in her head of how her pr…
A HoTT Quantum Equational Theory (Extended Version)
Jennifer Paykin, Steve Zdancewic
This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approac…
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…
A Linear/Producer/Consumer Model of Classical Linear Logic
Jennifer Paykin, Steve Zdancewic
This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding…
A static cost analysis for a higher-order language
N. Danner, J. Paykin, J. S. Royer
We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a…