131 citations · 343 across the 15 of their papers we have counts for
5 papers · 1 filter
Syntax Monads for the Working Formal Metatheorist
Lawrence Dunn, Val Tannen, Steve Zdancewic
Formally verifying the properties of formal systems using a proof assistant requires justifying numerous minor lemmas about capture-avoiding substitution. Despite work on category-…
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…
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi
Benoît Valiron, Steve Zdancewic
In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like la…