5 papers
TensorRocq: Enabling diagrammatic reasoning in Rocq
Benjamin Caldwell, William Spencer, Aleks Kissinger +1
Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams…
VyZX: Formal Verification of a Graphical Quantum Language
Adrian Lehmann, Ben Caldwell, Bhakti Shah +2
Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive d…
ViCAR: Visualizing Categories with Automated Rewriting in Coq
Bhakti Shah, Willam Spencer, Laura Zielinski +3
We present ViCAR, a library for working with monoidal categories in the Coq proof assistant. ViCAR provides definitions for categorical structures that users can instantiate with t…
Compositional Quantum Control Flow with Efficient Compilation in Qunity
Mikhail Mints, Finn Voichick, Leonidas Lampropoulos +1
Most existing quantum programming languages are based on the quantum circuit model of computation, as higher-level abstractions are particularly challenging to implement - especial…
COGNAC: Circuit Optimization via Gradients and Noise-Aware Compilation
Finn Voichick, Leonidas Lampropoulos, Robert Rand
We present COGNAC, a novel strategy for compiling quantum circuits based on numerical optimization algorithms from scientific computing. Observing that shorter-duration "partially…