论文标题
Quip-E程序的量子马尔可夫链语义
Quantum Markov Chain Semantics for Quip-E Programs
论文作者
论文摘要
在这项工作中，我们介绍了从量子编程语言拼写的片段（称为QUIP-E）到QPMC模型检查器的语义，旨在自动验证量子程序。作为主要结果，我们为与量子马尔可夫链相对应的QUIP-E语言定义了结构性操作语义，并将其用作通过QPMC模型检查器分析量子程序的基础。在开发从量子程序转换为量子马尔可夫链的工具的开发中证明了语义的属性。
In this work we present a mapping from a fragment of the quantum programming language Quipper, called Quip-E, to the semantics of the QPMC model checker, aiming at the automatic verification of quantum programs. As a main outcome, we define a structural operational semantics for the Quip-E language corresponding to quantum Markov chains, and we use it as a basis for analysing quantum programs through the QPMC model checker. The properties of the semantics are proved and contextualised in the development of a tool translating from quantum programs to quantum Markov chains.
