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
4 Pith papers cite this work, alongside 31 external citations. Polarity classification is still indexing.
4
Pith papers citing it
31
external citations · OpenAlex
representative 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.
Integer hybrid path-sums plus a sound Hoare logic enable semi-automated functional verification and expected-cost analysis of hybrid quantum programs with unbounded while loops.
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.
-
An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops
Integer hybrid path-sums plus a sound Hoare logic enable semi-automated functional verification and expected-cost analysis of hybrid quantum programs with unbounded while loops.