We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Quantum Physics

Title: VyZX : A Vision for Verifying the ZX Calculus

Abstract: 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 alternative to the quantum circuit model. Still, it carries no guarantee of its correctness. To address this, we developed VyZX, a verified ZX-calculus in the Coq proof assistant. VyZX provides two distinct representations of ZX diagrams for ease of programming and proof: A graph-based representation for writing high-level functions on diagrams and a block-based representation for proving ZX diagrams equivalent. Through these two different views, VyZX provides the tools necessary to verify properties and transformations of ZX diagrams. This paper explores the proofs and design choices underlying VyZX and its application and the challenges of verifying a graphical programming language.
Comments: 12 pages
Subjects: Quantum Physics (quant-ph); Programming Languages (cs.PL)
Cite as: arXiv:2205.05781 [quant-ph]
  (or arXiv:2205.05781v2 [quant-ph] for this version)

Submission history

From: Adrian Lehmann [view email]
[v1] Wed, 11 May 2022 21:37:23 GMT (257kb)
[v2] Wed, 18 May 2022 22:28:53 GMT (53kb)

Link back to: arXiv, form interface, contact.