44 citations · 47 across the 4 of their papers we have counts for
6 papers
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…