Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.
CoqQ : Foundational verification of quantum programs
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
fields
cs.PL 3verdicts
UNVERDICTED 3representative citing papers
Coq framework with discrete lenses for typed, compositional definition and verification of quantum circuits.
VyZX supplies a verified library that encodes inductive graphical languages to machine-check the soundness of ZX-calculus rewrite rules and supplies an IDE visualizer for diagrams.
citing papers explorer
-
Hybrid Path-Sums for Hybrid Quantum Programs
Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.
-
Typed compositional quantum computation with lenses
Coq framework with discrete lenses for typed, compositional definition and verification of quantum circuits.
-
VyZX: Formal Verification of a Graphical Quantum Language
VyZX supplies a verified library that encodes inductive graphical languages to machine-check the soundness of ZX-calculus rewrite rules and supplies an IDE visualizer for diagrams.