Robert Rand, University of Chicago

Abstract

We seek to verify the ZX-calculus, a powerful tool for representing and reasoning about quantum computation. ZX-diagrams are typically represented as adjacency-based graphs, reflecting the guiding principle that “only connectivity matters”. In the context of formal theorem provers like Coq, however, such graphs are difficult to reason about, especially when we seek to give them semantics. To address this gap, we introduce VyZX, a verified library for reasoning about the ZX-calculus, using inductive constructs that arise naturally from category theoretic definitions. We extend VyZX to reason about a variety of monoidal categories, provided they satisfy an appropriate set of coherence conditions, and show how to automate highly graphical proofs.

Speaker bio: Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. His research focuses on programming languages and verification for quantum computing and his main projects include the VOQC compiler for quantum circuits, the BellKAT quantum network language, and VyZX, a verified ZX calculus library. He also works on a range of verification projects, from adding automation to the Rocq proof assistant to developing quantum program logics. Robert developed and maintains the INQWIRE QuantumLib, an open-source library for verified quantum computing in Rocq, which underlies many of his projects including his online textbook, Verified Quantum Computing.