4 citations · 4 across the 2 of their papers we have counts for
4 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…
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…
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…
VyZX : A Vision for Verifying the ZX Calculus
Adrian Lehmann, Ben Caldwell, Robert Rand
Optimizing quantum circuits is a key challenge for quantum computing. The PyZX compiler broke new ground by optimizing circuits via the ZX calculus, a powerful graphical alternativ…