REVIEW 2 cited by
VyZX : A Vision for Verifying the ZX Calculus
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original 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.
Forward citations
Cited by 2 Pith papers
-
Laws of Quantum Programming
A formally verified collection of algebraic laws, normal forms, and a tail-recursion theorem for quantum programs, generalizing Hoare's classical laws.
-
Automating Equational Proofs in Dirac Notation
The paper gives a first-order theory of Dirac notation whose equations can be checked by a terminating, confluent rewrite system, implemented in DiracDec, with soundness proved in Coq.
Discussion (0). Continue with ORCID to comment.