CoqQ: Foundational Verification of Quantum Programs
summary
CoqQ is a Coq framework that formalizes a quantum language, proves a program logic sound with respect to a denotational semantics built on MathComp and MathComp Analysis, and supports arbitrary finite data types rather than only qubits. It implements labelled Dirac notation for local tensor reasoning, verifies canonical algorithms including the Hidden Subgroup Problem, and delivers machine-checked proofs ranging from single-line lemmas to several-hundred-line developments. The implementation is fully formalized in CoqQ.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:31Motivation
- 3:36Motivating Example: HSP
- 5:30Main Components
- 6:31(Abstract) Linear Algebra
- 7:10Tensor of Spaces
- 9:06Labeled Dirac Notation
- 10:24Automatic Lifting
- 12:07Quantum Framework
- 12:22qwhile Language
- 14:05Quantum Hoare Logic
- 15:56Inference Rules
- 17:02Code Metric
- 20:10Case Study
related talks
42mQuantum program analysis: Verification and Testing
15mToward A Quantum Programming Language for Higher Level Formal Verification
13mQbC: Quantum Correctness by Construction
22mEfficient Formal Verification of Quantum Error Correcting Programs
29mA Verified Optimizer for Quantum Circuits
28mA type-theoretic account of quantum computation (Extended Abstract)
22mQbC: Quantum Correctness by Construction
35mQuantum relational Hoare logic, towards a formalization