A First Step to the Categorical Logic of Quantum Programs
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) an...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2020-01-01
|
| Series: | Entropy |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1099-4300/22/2/144 |
| _version_ | 1811300050214584320 |
|---|---|
| author | Xin Sun Feifei He |
| author_facet | Xin Sun Feifei He |
| author_sort | Xin Sun |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T06:44:32Z |
| format | Article |
| id | doaj.art-2d367a41af0645c0b15aa9388551a0ed |
| institution | Directory Open Access Journal |
| issn | 1099-4300 |
| language | English |
| last_indexed | 2024-04-13T06:44:32Z |
| publishDate | 2020-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Entropy |
| spelling | doaj.art-2d367a41af0645c0b15aa9388551a0ed2022-12-22T02:57:37ZengMDPI AGEntropy1099-43002020-01-0122214410.3390/e22020144e22020144A First Step to the Categorical Logic of Quantum ProgramsXin Sun0Feifei He1Department of foundation of computer science, the John Paul II Catholic University of Lublin, 20-950 Lublin, PolandInstitute of logic and cognition, Sun Yat-sen University, Guangzhou 510970, ChinaThe 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.https://www.mdpi.com/1099-4300/22/2/144quantum logicquantum computingcategory theory |
| spellingShingle | Xin Sun Feifei He A First Step to the Categorical Logic of Quantum Programs Entropy quantum logic quantum computing category theory |
| title | A First Step to the Categorical Logic of Quantum Programs |
| title_full | A First Step to the Categorical Logic of Quantum Programs |
| title_fullStr | A First Step to the Categorical Logic of Quantum Programs |
| title_full_unstemmed | A First Step to the Categorical Logic of Quantum Programs |
| title_short | A First Step to the Categorical Logic of Quantum Programs |
| title_sort | first step to the categorical logic of quantum programs |
| topic | quantum logic quantum computing category theory |
| url | https://www.mdpi.com/1099-4300/22/2/144 |
| work_keys_str_mv | AT xinsun afirststeptothecategoricallogicofquantumprograms AT feifeihe afirststeptothecategoricallogicofquantumprograms AT xinsun firststeptothecategoricallogicofquantumprograms AT feifeihe firststeptothecategoricallogicofquantumprograms |