A proof system for disjoint parallel quantum programs

被引：10
作者：
Ying, Mingsheng [1 ,2 ]
Zhou, Li [3 ]
Li, Yangjia [1 ]
Feng, Yuan [4 ]
机构：
[1] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China
[2] Tsinghua Univ, Dept Comp Sci & Technol, Beijing, Peoples R China
[3] Max Planck Inst Secur & Privacy, Berlin, Germany
[4] Univ Technol Sydney, Ctr Quantum Software & Informat, Sydney, NSW, Australia
来源：
THEORETICAL COMPUTER SCIENCE | 2022年 / 897卷
关键词：
Quantum programming; Quantum Hoare logic; Parallel programs; Entanglement; LOGIC; VERIFICATION; CORRECTNESS; COMPUTATION;
D O I：
10.1016/j.tcs.2021.10.025
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper, we define the operational and denotational semantics of a special class of parallel quantum programs, namely disjoint parallel quantum programs. Based on them, a proof system for reasoning about disjoint parallel quantum programs is developed, which is (relatively) complete even when entanglement between different processes appears in the preconditions and postconditions. (C) 2021 Elsevier B.V. All rights reserved.
引用
收藏
页码：164 / 184
页数：21
相关论文
共 42 条
[1]  
Aharonov D., 2017, ARXIV170701187
[2]  
[Anonymous], 1972, Operating Systems Techniques
[3]  
Apt Krzysztof R., 2009, Verification of Sequential and Concurrent Programs
[4]   LQP: the dynamic logic of quantum information [J].
Baltag, Alexandru ;
Smets, Sonja .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2006, 16 (03) :491-525
[5]   Relational Proofs for Quantum Programs [J].
Barthe, Gilles ;
Hsu, Justin ;
Ying, Mingsheng ;
Yu, Nengkun ;
Zhou, Li .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL)
[6]   Efficient distributed quantum computing [J].
Beals, Robert ;
Brierley, Stephen ;
Gray, Oliver ;
Harrow, Aram W. ;
Kutin, Samuel ;
Linden, Noah ;
Shepherd, Dan ;
Stather, Mark .
PROCEEDINGS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2013, 469 (2153)
[7]   Quantum nonlocality without entanglement [J].
Bennett, CH ;
DiVincenzo, DP ;
Fuchs, CA ;
Mor, T ;
Rains, E ;
Shor, PW ;
Smolin, JA ;
Wootters, WK .
PHYSICAL REVIEW A, 1999, 59 (02) :1070-1091
[8]   Separability of very noisy mixed states and implications for NMR Quantum computing [J].
Braunstein, SL ;
Caves, CM ;
Jozsa, R ;
Linden, N ;
Popescu, S ;
Schack, R .
PHYSICAL REVIEW LETTERS, 1999, 83 (05) :1054-1057
[9]   Quantum advantage with shallow circuits [J].
Bravyi, Sergey ;
Gosset, David ;
Koenig, Robert .
SCIENCE, 2018, 362 (6412) :308-+
[10]   Dynamic quantum logic for quantum programs [J].
Brunet, O ;
Jorrand, P .
INTERNATIONAL JOURNAL OF QUANTUM INFORMATION, 2004, 2 (01) :45-54
12345