{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T02:08:53Z","timestamp":1785290933503,"version":"3.55.0"},"reference-count":37,"publisher":"MDPI AG","issue":"2","license":[{"start":{"date-parts":[[2020,1,24]],"date-time":"2020-01-24T00:00:00Z","timestamp":1579824000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Entropy"],"abstract":"<jats:p>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\u2019s algorithm and the concealing property of quantum bit commitment.<\/jats:p>","DOI":"10.3390\/e22020144","type":"journal-article","created":{"date-parts":[[2020,1,24]],"date-time":"2020-01-24T11:01:00Z","timestamp":1579863660000},"page":"144","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A First Step to the Categorical Logic of Quantum Programs"],"prefix":"10.3390","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9320-2522","authenticated-orcid":false,"given":"Xin","family":"Sun","sequence":"first","affiliation":[{"name":"Department of foundation of computer science, the John Paul II Catholic University of Lublin, 20-950 Lublin, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Feifei","family":"He","sequence":"additional","affiliation":[{"name":"Institute of logic and cognition, Sun Yat-sen University, Guangzhou 510970, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2020,1,24]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"1608","DOI":"10.1016\/j.ic.2007.08.001","article-title":"Probabilistic bisimulations for quantum processes","volume":"205","author":"Feng","year":"2007","journal-title":"Inf. Comput."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/1507244.1507249","article-title":"An algebra of quantum processes","volume":"10","author":"Ying","year":"2009","journal-title":"ACM Trans. Comput. Log."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1145\/2400676.2400680","article-title":"Bisimulation for Quantum Processes","volume":"34","author":"Feng","year":"2012","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1016\/j.jsc.2015.05.001","article-title":"Semi-automated verification of security proofs of quantum cryptographic protocols","volume":"73","author":"Kubota","year":"2016","journal-title":"J. Symb. Comput."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"823","DOI":"10.2307\/1968621","article-title":"The Logic of Quantum Mechanics","volume":"37","author":"Birkhoff","year":"1936","journal-title":"Ann. Math."},{"key":"ref_6","first-page":"439","article-title":"Axiomatique quantique","volume":"37","author":"Piron","year":"1964","journal-title":"Helv. Phys. Acta"},{"key":"ref_7","first-page":"165","article-title":"Quantum experiments and the lattice of orthomodular logics","volume":"35","author":"Malinowski","year":"1999","journal-title":"Log. Anal."},{"key":"ref_8","first-page":"11","article-title":"On the lattice of orthomodular logics","volume":"28","author":"Malinowski","year":"1999","journal-title":"Bull. Sect. Log."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s11225-006-7202-2","article-title":"MV-Algebras and Quantum Computation","volume":"82","author":"Ledda","year":"2006","journal-title":"Stud. Log."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/s11225-007-9079-0","article-title":"Expanding Quasi-MV Algebras by a Quantum Operator","volume":"87","author":"Giuntini","year":"2007","journal-title":"Stud. Log."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1023\/A:1023327005274","article-title":"Quantum Computational Logic","volume":"42","author":"Gudder","year":"2003","journal-title":"Int. J. Theor. Phys."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/s10992-013-9273-7","article-title":"Editors\u2019 Introduction: The Third Life of Quantum Logic: Quantum Logic Inspired by Quantum Computing","volume":"42","author":"Dunn","year":"2013","journal-title":"J. Philos. Log."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1142\/S0219749904000067","article-title":"Dynamic quantum logic for quantum programs","volume":"2","author":"Brunet","year":"2004","journal-title":"Int. J. Quantum Inf."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2006.04.003","article-title":"Reasoning About Imperative Quantum Programs","volume":"158","author":"Chadha","year":"2006","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/j.tcs.2007.06.011","article-title":"Proof rules for the correctness of quantum programs","volume":"386","author":"Feng","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"19:1","DOI":"10.1145\/2049706.2049708","article-title":"Floyd-hoare logic for quantum programs","volume":"33","author":"Ying","year":"2011","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"2267","DOI":"10.1007\/s10773-005-8022-2","article-title":"Complete Axiomatizations for Quantum Actions","volume":"44","author":"Baltag","year":"2005","journal-title":"Int. J.Theor. Phys."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1017\/S0960129506005299","article-title":"LQP: The dynamic logic of quantum information","volume":"16","author":"Baltag","year":"2006","journal-title":"Math. Struct. Comput. Sci."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s11225-008-9126-5","article-title":"A Dynamic-Logical Perspective on Quantum Behavior","volume":"89","author":"Baltag","year":"2008","journal-title":"Stud. Log."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"3628","DOI":"10.1007\/s10773-013-1987-3","article-title":"PLQP & Company: Decidable Logics for Quantum Algorithms","volume":"53","author":"Baltag","year":"2014","journal-title":"Int. J. Theor. Phys."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"1421","DOI":"10.1007\/s00500-015-1802-6","article-title":"Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs","volume":"21","author":"Bergfeld","year":"2017","journal-title":"Soft. Comput."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"3991","DOI":"10.1007\/s10773-017-3409-4","article-title":"A Logical Analysis of Quantum Voting Protocols","volume":"56","author":"Rad","year":"2017","journal-title":"Int. J. Theor. Phys."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Abramsky, S., and Coecke, B. (2004, January 14\u201317). A Categorical Semantics of Quantum Protocols. Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland.","DOI":"10.1109\/LICS.2004.1319636"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1088\/1367-2630\/13\/4\/043016","article-title":"Interacting quantum observables: Categorical algebra and diagrammatics","volume":"13","author":"Coecke","year":"2011","journal-title":"New J. Phys."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"5179","DOI":"10.1007\/s11128-014-0837-4","article-title":"Categories of quantum and classical channels","volume":"15","author":"Coecke","year":"2016","journal-title":"Quantum Inf. Process."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Coecke, B., and Kissinger, A. (2017). Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning, Cambridge University Press.","DOI":"10.1017\/9781316219317"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-70583-3_25","article-title":"Interacting Quantum Observables","volume":"Volume 5126","author":"Coecke","year":"2008","journal-title":"International Colloquium on Automata, Languages, and Programming"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"093021","DOI":"10.1088\/1367-2630\/16\/9\/093021","article-title":"The ZX-calculus is complete for stabilizer quantum mechanics","volume":"16","author":"Backens","year":"2014","journal-title":"New J. Phys."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Jeandel, E., Perdrix, S., and Vilmart, R. (2018, January 12). A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics. Proceedings of the Thirty-Third Annual ACM\/IEEE Symposium on Logic in Computer Science, Oxford, UK.","DOI":"10.1145\/3209108.3209131"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Hadzihasanovic, A., Ng, K.F., and Wang, Q. (2018, January 12). Two complete axiomatisations of pure-state qubit quantum computing. Proceedings of the Thirty-Third Annual ACM\/IEEE Symposium on Logic in Computer Science, Oxford, UK.","DOI":"10.1145\/3209108.3209128"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1142\/S0219749903000383","article-title":"Quantum walks and their algorithmic applications","volume":"1","author":"Ambainis","year":"2003","journal-title":"Int. J. Quantum Inf."},{"key":"ref_32","unstructured":"Backens, M. (2015, January 15\u201317). The ZX-calculus is complete for the single-qubit Clifford+T group. Proceedings of the 12th International Conference on Quantum Physics and Logic, Oxford, UK."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Yanofsky, N., and Mannucci, M. (2008). Quantum Computing for Computer Scientists, Cambridge University Press.","DOI":"10.1017\/CBO9780511813887"},{"key":"ref_34","unstructured":"Bennetta, C., and Brassard, G. (1984, January 9\u201312). Quantum cryptography: Public key distribution and coin tossing. Proceedings of the IEEE International Conference on Computers, Systems and Signal Processing, Bangalore, India."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"3414","DOI":"10.1103\/PhysRevLett.78.3414","article-title":"Unconditionally secure quantum bit commitment is impossible","volume":"78","author":"Mayers","year":"1997","journal-title":"Phys. Rev. Lett."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"3410","DOI":"10.1103\/PhysRevLett.78.3410","article-title":"Is Quantum Bit Commitment Really Possible?","volume":"78","author":"Lo","year":"1997","journal-title":"Phys. Rev. Lett."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"012310","DOI":"10.1103\/PhysRevA.65.012310","article-title":"Degrees of concealment and bindingness in quantum bit commitment protocols","volume":"65","author":"Spekkens","year":"2001","journal-title":"Phys. Rev. A"}],"container-title":["Entropy"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1099-4300\/22\/2\/144\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T13:44:36Z","timestamp":1760363076000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1099-4300\/22\/2\/144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,24]]},"references-count":37,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2020,2]]}},"alternative-id":["e22020144"],"URL":"https:\/\/doi.org\/10.3390\/e22020144","relation":{},"ISSN":["1099-4300"],"issn-type":[{"value":"1099-4300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,1,24]]}}}