REVIEW 1 cited by
CoqQ: Foundational Verification of Quantum Programs
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
CoqQ: Foundational Verification of Quantum Programs
read the original abstract
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (mathcomp and mathcomp analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.
Forward citations
Cited by 1 Pith paper
-
Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
A Mathlib-compatible Lean 4 library formalizes the DPI for sandwiched Rényi relative entropy on finite-dimensional systems and supplies reusable quantum-information infrastructure.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.