An Expressive Assertion Language for Quantum Programs
Abstract
In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques such as Gödelization to prove that this language is expressive with respect to the quantum programs with loops–specifically, for any program S and any postcondition ψ formulated in the assertion language, the weakest precondition of S with respect to ψ can also be expressed as a formula in the assertion language. As an application, we present a sound and relatively complete quantum Hoare logic upon our expressive assertion language.
Fields of Study & Subjects
Quantum Computing Algorithms and Architecture
Logic
Reasoning
and Knowledge
Quantum Mechanics and Applications
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Publisher
- Association for Computing Machinery (ACM)
- Volume
- 10
- Issue
- POPL
- Pages
- 444–475
- Publication date
- 8 January 2026
- Language
- EN