A First Step to the Categorical Logic of Quantum Programs

被引：1
|
作者：
Sun, Xin [1 ]
He, Feifei [2 ]
机构：
[1] John Paul II Catholic Univ Lublin, Dept Fdn Comp Sci, PL-20950 Lublin, Poland
[2] Sun Yat Sen Univ, Inst Log & Cognit, Guangzhou 510970, Peoples R China
来源：
ENTROPY | 2020年 / 22卷 / 02期
关键词：
quantum logic; quantum computing; category theory; BIT COMMITMENT; CORRECTNESS;
D O I：
10.3390/e22020144
中图分类号：
O4 [物理学];
学科分类号：
0702 ;
摘要：
The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. We present the syntax, semantics and proof system of CLQP. As a proof-of-concept, we apply CLQP to verify the correctness of Deutsch's algorithm and the concealing property of quantum bit commitment.
引用
收藏
页数：14
相关论文
共 50 条
  • [41] CATEGORICAL COMBINATORY-LOGIC
    CURIEN, PL
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 194 : 130 - 139
  • [42] Categorical consequence for paraconsistent logic
    Johnson, F
    Woodruff, PW
    PARACONSISTENCY: THE LOGICAL WAY TO THE INCONSISTENT, 2002, 228 : 141 - 150
  • [43] Streaming transfer of mobile programs in first order linear logic
    Murakami, M
    ISAS/CITSA 2004: INTERNATIONAL CONFERENCE ON CYBERNETICS AND INFORMATION TECHNOLOGIES, SYSTEMS AND APPLICATIONS AND 10TH INTERNATIONAL CONFERENCE ON INFORMATION SYSTEMS ANALYSIS AND SYNTHESIS, VOL 1, PROCEEDINGS: COMMUNICATIONS, INFORMATION TECHNOLOGIES AND COMPUTING, 2004, : 275 - 280
  • [44] Protected completions of first-order general logic programs
    1600, (06):
  • [45] First-order modular logic programs and their conservative extensions
    Harrison, Amelia
    Lierler, Yuliya
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2016, 16 : 755 - 770
  • [46] Representing first-order causal theories by logic programs
    Ferraris, Paolo
    Lee, Joohyung
    Lierler, Yuliya
    Lifschitz, Vladimir
    Yang, Fangkai
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2012, 12 : 383 - 412
  • [47] A CATEGORICAL INTERPRETATION OF PARTIAL FUNCTION LOGIC AND HOARE LOGIC
    KNIJNENBURG, PMW
    NORDEMANN, F
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 620 : 229 - 240
  • [48] A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
    Le, Xuan-Bach
    Lin, Shang-Wei
    Sun, Jun
    Sanan, David
    Proceedings of the ACM on Programming Languages, 2022, 6 (POPL)
  • [49] A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
    Le, Xuan-Bach
    Lin, Shang-Wei
    Sun, Jun
    Sanan, David
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6
  • [50] TRANSFORMING NORMAL LOGIC PROGRAMS TO CONSTRAINT LOGIC PROGRAMS
    KANCHANASUT, K
    STUCKEY, PJ
    THEORETICAL COMPUTER SCIENCE, 1992, 105 (01) : 27 - 56
12345