一句话：提出量子分离合取的量子解释，并构建支持局部推理的 Hoare 风格量子程序验证框架。
量子程序的设计与验证十分困难：量子态规模随量子比特数指数增长，且需要复杂数学来编码与操作，导致状态空间爆炸。为支持量子程序的局部推理，本文提出一个 Hoare 风格的推理框架。其核心是给出分离逻辑中分离合取（separating conjunction）的量子解释，从而将分离逻辑融入框架，并设计一个与经典 frame rule 类似的量子 frame rule。基于该规则，可以只关注程序局部涉及的量子态与资源，缓解整体状态空间爆炸。作者将该框架应用于多个量子程序验证，包括 Deutsch–Jozsa 算法和 Grover 算法，表明其可用于验证非平凡的量子算法。
It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.
@article{paperbot1562,
title = {A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic},
author = {Xuan-Bach Le and Shang-Wei Lin and Jun Sun and David Sanan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498697}
}