一句话：提出 Bunched Logic 的量子模型，并构建量子分离逻辑以验证量子程序安全性。
该论文为子结构逻辑 Bunched Implications（BI）提出一种适用于量子态推理的模型：BI 的分离合取被解释为可分离量子态，从而将分离逻辑思想推广到量子领域。作者据此设计程序逻辑，其前后条件均为描述量子态的 BI 公式，可视为命令式量子程序的分离逻辑对应物。该逻辑被用于证明量子一次性密码本与秘密共享的安全性，并用于发现 Google Cirq 变分量子算法（VQA）教程中的一处缺陷。结果表明，BI 的量子解释能为量子程序安全和量子软件开发提供有效的形式化推理工具。
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states—the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirq’s tutorial on the Variational Quantum Algorithm (VQA).
DOI 原文 ·
@inproceedings{paperbot6215,
title = {A Quantum Interpretation of Bunched Logic & Quantum Separation Logic},
author = {Li Zhou and Gilles Barthe and Justin Hsu and Mingsheng Ying and Nengkun Yu},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470673}
}