一句话：在 Coq 中构建深度嵌入的量子编程语言与程序逻辑，并机器化证明其相对于指称语义的可靠性。
该论文提出 CoqQ，一个在 Coq 证明助手中推理量子程序的框架。其核心包括一个深度嵌入的量子编程语言，可便捷表达经典量子算法，以及一个表达力强的程序逻辑，用于证明程序性质。CoqQ 具有基础性：程序逻辑相对于基于 MathComp 与 MathComp Analysis 的指称语义被形式化证明为可靠。它也注重实用性：断言可使用 Dirac 表达式以简化规约，证明可利用局部与并行推理以减少验证工作量。论文通过文献中的多个实例展示了 CoqQ 的适用性。
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.
@article{paperbot2081,
title = {CoqQ: Foundational Verification of Quantum Programs},
author = {Li Zhou and Gilles Barthe and Pierre-Yves Strub and Junyi Liu and Mingsheng Ying},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571222}
}