一句话：提出以广义Pauli算子准概率分布表示量子谓词的断言语言，可表达含循环量子程序的最弱前置条件，并建立可靠且相对完备的量子Hoare逻辑。
该文研究基于期望的量子程序推理，针对其缺乏表达力强的断言语言这一问题，设计了一种新的断言语言。其核心思想是用广义Pauli算子的准概率分布来表示量子谓词，从而刻画期望型推理中的断言。为证明语言的表达力，作者将经典的Gödel化技巧推广到量子设定，证明对任意含循环的量子程序S以及以该语言写成的后置条件ψ，S关于ψ的最弱前置条件同样可用该语言中的公式表达。作为应用，作者在该富有表达力的断言语言之上给出了一个可靠且相对完备的量子Hoare逻辑。
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.
@article{SuFYZ26,
title = {An Expressive Assertion Language for Quantum Programs},
author = {Bonan Su and Yuan Feng and Mingsheng Ying and Li Zhou},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776658}
}