qKleene: Verification of Quantum RAM Made Easy
summary
qKleene is a small language that encodes control flow as regular-expression-like programs combining unbounded classical integers and bounded quantum registers of k qubits, with induction-defined semantics for concatenation, choice and iteration. It gives a concrete collecting semantics (measurement can be probabilistic or pick-most-probable), a Hoare-style proof system for invariants (example: a qflip loop proving alternation between product and entangled states), and a prototype abstract-interpretation-ready framework — an abstract interpreter is straightforward to build.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:36What Is Program Analysis
- 5:30Completeness and Incompleteness
- 6:56What Is a Program in Q Clean
- 9:00Structure of the Basic Expressions
related talks
35mQuantum relational Hoare logic, towards a formalization
13mQbC: Quantum Correctness by Construction
22mCoqQ: Foundational Verification of Quantum Programs
42mQuantum program analysis: Verification and Testing
22mQbC: Quantum Correctness by Construction
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
17mAn Algebraic Language for Specifying Quantum Networks
20mQuantum Register Machine: Efficient Implementation of Quantum Recursive Programs