Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
summary
Encodes quantum while programs into algebraic expressions and proves soundness: derivability in non-idempotent Kleene algebra implies denotational equivalence, with a completeness theorem relative to any quantum interpretation. Builds a quantum path model that lifts states and channels to multisets and monotone linear maps so the star is always defined. Extends the algebra to NKA with tests using an effect algebra and partitions, gives an algebraic proof of the single-while normalization theorem, and verifies loop-unrolling under projective measurements.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:39Quantum While-Programs Equivalences
- 2:08KAT-like Algebraic Reasoning
- 2:58Algebraic Reasoning via NKA
- 3:44Structure of Concepts
- 5:00Non-idempotent Kleene Algebra
- 6:46Encoding Quantum While-Programs
- 7:53Quantum Path Model
- 9:12Quantum Interpretation
- 10:19Verifying Compiler Rule
- 11:27Quantum Bohm-Jacopini Theorem
- 13:17Propositional Quantum Hoare Logic
- 14:02Future Directions
related talks
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
42mQuantum program analysis: Verification and Testing
17mAn Algebraic Language for Specifying Quantum Networks
16mqKleene: Verification of Quantum RAM Made Easy
14mDenotational semantics for stabiliser quantum programs
22mQbC: Quantum Correctness by Construction
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
13mQbC: Quantum Correctness by Construction