An Expressive Assertion Language for Quantum Programs
summary
Defines an assertion language that represents quantum predicates as quasi-probability distributions of generalized Pauli operators and proves constructively that for any QI program with loops the weakest precondition always expressible as a formula in the language. Uses Gödelization style encodings of rational sequences, sup/inf to capture limits, and reductions of compositions to coefficient summations and inner products. Delivers a sound and relatively complete quantum Hoare logic built on that expressiveness.
AI-written summary · about
chapters (9)
- 0:00Quantum assertion language intro
- 1:49Quantum programs and QI language
- 4:02Program specs and weakest preconditions
- 8:53Expressiveness of quantum assertions
- 9:38Assertion language syntax
- 12:32Expressiveness for while loops
- 20:48Weakest preconditions for quantum
- 22:16Conclusion and Hoare logic
- 23:23Q&A
related talks
13mQbC: Quantum Correctness by Construction
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
15mToward A Quantum Programming Language for Higher Level Formal Verification
35mQuantum relational Hoare logic, towards a formalization
15mAssertion-Based Optimization of Quantum Programs
42mQuantum program analysis: Verification and Testing
22mQbC: Quantum Correctness by Construction