{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:04Z","timestamp":1781238904477,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T00:00:00Z","timestamp":1649203200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2018YFA0306701"],"award-info":[{"award-number":["2018YFA0306701"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","award":["DP220102059 and DP180100691"],"award-info":[{"award-number":["DP220102059 and DP180100691"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,7,31]]},"abstract":"<jats:p>Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.<\/jats:p>","DOI":"10.1145\/3517145","type":"journal-article","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T11:41:29Z","timestamp":1648554089000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Verification of Distributed Quantum Programs"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3097-3896","authenticated-orcid":false,"given":"Yuan","family":"Feng","sequence":"first","affiliation":[{"name":"University of Technology Sydney, Broadway, Ultimo NSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjiang","family":"Li","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Broadway, Ultimo NSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, China and Tsinghua University, Haidian, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,6]]},"reference":[{"key":"e_1_3_3_2_1","volume-title":"Verification of Sequential and Concurrent Programs","author":"Apt Krzysztof","year":"2010","unstructured":"Krzysztof Apt, Frank S. De Boer, and Ernst-R\u00fcdiger Olderog. 2010. Verification of Sequential and Concurrent Programs. Springer Science & Business Media."},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/5956.6000"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90001-9"},{"key":"e_1_3_3_5_1","volume-title":"Proceedings of the International Conference on Computers, Systems and Signal Processing","author":"Bennett Charles H.","year":"1984","unstructured":"Charles H. Bennett and Gilles Brassard. 1984. Quantum cryptography: Public key distribution and coin tossing. In Proceedings of the International Conference on Computers, Systems and Signal Processing."},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.76.722"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.69.2881"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.81.5932"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-qtc.2020.0002"},{"key":"e_1_3_3_14_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","year":"1976","unstructured":"Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice-Hall Englewood Cliffs."},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.62.052317"},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.08.001"},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2400676.2400680"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1038\/46503"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458817.3476172"},{"key":"e_1_3_3_23_1","volume-title":"A Practical Theory of Programming","author":"Hehner Eric C. R.","year":"2012","unstructured":"Eric C. R. Hehner. 2012. A Practical Theory of Programming. Springer Science & Business Media."},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.101.240501"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/977091.977108"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature07127"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3345312.3345497"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12732-1"},{"key":"e_1_3_3_32_1","volume-title":"Quantum Computation and Quantum Information","author":"Nielsen Michael A.","year":"2002","unstructured":"Michael A. Nielsen and Isaac Chuang. 2002. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_3_3_33_1","article-title":"Quantum algorithms and simulation for parallel and distributed quantum computing","author":"Parekh Rhea","year":"2021","unstructured":"Rhea Parekh, Andrea Ricciardi, Ahmed Darwish, and Stephen DiAdamo. 2021. Quantum algorithms and simulation for parallel and distributed quantum computing. arXiv preprint arXiv:2106.06841 (2021).","journal-title":"arXiv preprint arXiv:2106.06841"},{"key":"e_1_3_3_34_1","doi-asserted-by":"publisher","DOI":"10.1038\/nphoton.2015.154"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.abg1919"},{"key":"e_1_3_3_36_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.86.5188"},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.10.008"},{"key":"e_1_3_3_39_1","first-page":"581","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"Tani Seiichiro","year":"2005","unstructured":"Seiichiro Tani, Hirotada Kobayashi, and Keiji Matsumoto. 2005. Exact quantum algorithms for the leader election problem. In Annual Symposium on Theoretical Aspects of Computer Science. Springer, 581\u2013592."},{"key":"e_1_3_3_40_1","first-page":"1","volume-title":"2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","author":"Unruh Dominique","year":"2019","unstructured":"Dominique Unruh. 2019. Quantum Hoare logic with ghost variables. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1\u201313."},{"key":"e_1_3_3_41_1","volume-title":"Mathematical Foundations of Quantum Mechanics","author":"Neumann John von","year":"1955","unstructured":"John von Neumann. 1955. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ."},{"key":"e_1_3_3_42_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aam9288"},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1038\/299802a0"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_3_45_1","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","year":"2016","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann."},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0465-3"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"issue":"2","key":"e_1_3_3_48_1","first-page":"64","article-title":"Normalform-Transformationen f\u00fcr CSP-Programme","volume":"3","author":"Zoebel Dieter","year":"1988","unstructured":"Dieter Zoebel. 1988. Normalform-Transformationen f\u00fcr CSP-Programme. Informatik (Berlin, West) 3, 2 (1988), 64\u201376.","journal-title":"Informatik (Berlin, West)"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3517145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3517145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:02Z","timestamp":1750183742000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3517145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,6]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,7,31]]}},"alternative-id":["10.1145\/3517145"],"URL":"https:\/\/doi.org\/10.1145\/3517145","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,6]]},"assertion":[{"value":"2021-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}