{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:35:58Z","timestamp":1791459358685,"version":"4.3.4"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T00:00:00Z","timestamp":1781654400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2023YFA1009403"],"award-info":[{"award-number":["2023YFA1009403"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,7,31]]},"abstract":"<jats:p>\n                    In this article, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.\u2019s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum)\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\mathbf{if}}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    -statements and the unfolding of nested (quantum)\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\mathbf{if}}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    -statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\mathbf{while}}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    -loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits.\n                  <\/jats:p>\n                  <jats:p>We expect that these laws can be utilised in correctness-preserving transformation, compilation and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum programme development.<\/jats:p>","DOI":"10.1145\/3765903","type":"journal-article","created":{"date-parts":[[2025,9,18]],"date-time":"2025-09-18T18:43:53Z","timestamp":1758221033000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Laws of Quantum Programming"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"Centre for Quantum Software and Information, University of Technology Sydney, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy, Bochum, Germany and IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,17]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Ali J. Abhari Arvin Faruque Mohammad J. Dousti Lukas Svec Oana Catu Amlan Chakrabati Chen-Fu Chiang Seth Vanderwilt John Black and Fred Chong. 2012. Scaffold: Quantum Programming Language. Technical Report. Princeton University."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.04.001"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_10"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_3_11_2","first-page":"53","volume-title":"Boogie 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot Fran\u00e7ois","year":"2011","unstructured":"Fran\u00e7ois Bobot, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, and Andrei Paskevich. 2011. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, 53\u201364. Retrieved from https:\/\/inria.hal.science\/hal-00790310"},{"key":"e_1_3_3_12_2","article-title":"Isabelle marries dirac: A library for quantum computation and quantum information","author":"Bordg Anthony","year":"2020","unstructured":"Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Arch. Formal Proofs. arXiv:2110.01320. Retrieved from https:\/\/arxiv.org\/pdf\/2110.01320","journal-title":"Arch. Formal Proofs"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656430"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","unstructured":"Christophe Chareton S\u00e9bastien Bardin Dong Ho Lee Beno\u00eet Valiron Renaud Vilmart and Zhaowei Xu. 2023. Formal Methods for Quantum Algorithms. In Handbook of Formal Analysis and Verification in Cryptography. CRC Press 319\u2013422. Retrieved from https:\/\/cea.hal.science\/cea-04479879","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.127.100501"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2025. Cirq. DOI: 10.5281\/zenodo.15191735","DOI":"10.5281\/zenodo.15191735"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785834"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_3_23_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","year":"1976","unstructured":"Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Edsger Wybe Dijkstra, Etats-Unis Informaticien, and Edsger Wybe Dijkstra. 1976. A Discipline of Programming, Vol. 613924118. Prentice-Hall, Englewood Cliffs."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2020-06-04-279"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582039"},{"key":"e_1_3_3_26_2","unstructured":"Yuan Feng Li Zhou and Yingte Xu. 2023. Refinement calculus of quantum programs with projective assertions. arXiv:2311.14215. Retrieved from https:\/\/arxiv.org\/abs\/2311.14215"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.2478\/v10175-010-0008-4"},{"key":"e_1_3_3_28_2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1007\/978-3-319-02297-0_9","volume-title":"Computer Algebra in Scientific Computing","author":"Gerdt Vladimir P.","year":"2013","unstructured":"Vladimir P. Gerdt and Alexander N. Prokopenya. 2013. Simulation of quantum error correction with mathematica. In Computer Algebra in Scientific Computing. Vladimir P. Gerdt, Wolfram Koepf, Ernst W. Mayr, and Evgenii V. Vorozhtsov (Eds.), Springer International Publishing, Cham, 116\u2013129."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TQE.2023.3275868"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","unstructured":"Kesha Hietala Robert Rand Shih-Han Hung Xiaodi Wu and Michael Hicks. 2021. A verified optimizer for quantum circuits. Proc. ACM Program. Lang. 5 POPL Article 37 (Jan. 2021) 29 pages. DOI: 10.1145\/3434318","DOI":"10.1145\/3434318"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_3_3_35_2","unstructured":"Ali Javadi-Abhari Matthew Treinish Kevin Krsulich Christopher J. Wood Jake Lishman Julien Gacon Simon Martiel Paul D. Nation Lev S. Bishop Andrew W. Cross et al. 2024. Quantum computing with Qiskit. arXiv:240508810. Retrieved from https:\/\/arxiv.org\/abs\/2405.08810"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_3_3_38_2","unstructured":"Aleks Kissinger and John van de Wetering. 2024. Picturing Quantum Software: An Introduction to the ZX-Calculus and Quantum Compilation. Manuscript submitted for review."},{"key":"e_1_3_3_39_2","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/978-3-319-21401-6_22","volume-title":"Automated Deduction (CADE \u201925)","author":"Kissinger Aleks","year":"2015","unstructured":"Aleks Kissinger and Vladimir Zamdzhiev. 2015. Quantomatic: A Proof Assistant for Diagrammatic Reasoning. In Automated Deduction (CADE \u201925), Amy P. Felty and Aart Middeldorp (Eds.), Springer International Publishing, Cham, 326\u2013336."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_3_41_2","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX: A vision for verifying the ZX calculus. arXiv:220505781. Retrieved from https:\/\/arxiv.org\/abs\/2205.05781"},{"key":"e_1_3_3_42_2","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: formal verification of a graphical quantum language. arXiv:231111571. Retrieved from https:\/\/arxiv.org\/abs\/2311.11571"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2022. Mathematical components. DOI: 10.5281\/zenodo.7118596","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_3_3_46_2","volume-title":"Quantum Programming Language LanQ","author":"Mlnar\u0131k Hynek","year":"2007","unstructured":"Hynek Mlnar\u0131k. 2007. Quantum Programming Language LanQ. Masaryk University-Faculty of Informatics, Czech Republic."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.5555\/95423"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3117515"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10773-005-7071-x"},{"key":"e_1_3_3_51_2","first-page":"846","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917)","author":"Paykin Jennifer","year":"2017","unstructured":"Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: A core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917), Giuseppe Castagna and Andrew D. Gordon (Eds.), ACM, 846\u2013858. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=3009894"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3720433"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","unstructured":"Yuxiang Peng Kesha Hietala Runzhou Tao Liyi Li Robert Rand Michael Hicks and Xiaodi Wu. 2023. A formally certified end-to-end implementation of Shor\u2019s factorization algorithm. Proceedings of the National Academy of Sciences 120 21 e2218775120. DOI: 10.1073\/pnas.2218775120","DOI":"10.1073\/pnas.2218775120"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523713"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90049-7"},{"key":"e_1_3_3_58_2","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-319-89366-2_19","volume-title":"Foundations of Software Science and Computation Structures","author":"Sabry Amr","year":"2018","unstructured":"Amr Sabry, Beno\u00eet Valiron, and Juliana Kaizer Vizzotto. 2018. From symmetric pattern-matching to quantum control. In Foundations of Software Science and Computation Structures. Christel Baier and Ugo Dal Lago (Eds.), Springer International Publishing, Cham, 348\u2013364."},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_6"},{"key":"e_1_3_3_60_2","unstructured":"Bhakti Shah William Spencer Laura Zielinski Ben Caldwell Adrian Lehmann and Robert Rand. 2024. ViCAR: visualizing categories with automated rewriting in Coq. arXiv:240408163. Retrieved from https:\/\/arxiv.org\/abs\/2404.08163"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/1120725.1120847"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab8e92"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_3_64_2","unstructured":"Korbinian Staudacher. 2021. Optimization Approaches for Quantum Circuits Using ZX-Calculus. Ph.D. Dissertation. Master\u2019s Thesis Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-01-31-49"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2023. The Coq Proof Assistant. DOI: 10.5281\/zenodo.8161141","DOI":"10.5281\/zenodo.8161141"},{"key":"e_1_3_3_69_2","unstructured":"The MathComp Analysis Development Team. 2024. MathComp-Analysis: Mathematical Components Compliant Analysis Library. Retrieved from https:\/\/github.com\/math-comp\/analysis (Since 2017. Version 1.0.0)."},{"key":"e_1_3_3_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64837-4_11"},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100790"},{"key":"e_1_3_3_73_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397246"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591254"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_3_77_2","unstructured":"Zhaowei Xu Mingsheng Ying and Beno\u00eet Valiron. 2021. Reasoning about recursive quantum programs. arXiv:2107.11679. Retrieved from https:\/\/arxiv.org\/abs\/2107.11679"},{"key":"e_1_3_3_78_2","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_79_2","unstructured":"Mingsheng Ying Nengkun Yu and Yuan Feng. 2012. Defining quantum control flow. arXiv:1209.4379. Retrieved from https:\/\/arxiv.org\/abs\/1209.4379"},{"key":"e_1_3_3_80_2","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying and Zhicheng Zhang. 2023. Quantum recursive programming with quantum case statements. arXiv:231101725. Retrieved from https:\/\/arxiv.org\/abs\/2311.01725","DOI":"10.2139\/ssrn.4705308"},{"key":"e_1_3_3_81_2","unstructured":"Mingsheng Ying and Zhicheng Zhang. 2024. Verification of recursively defined quantum circuits. arXiv:240405934. Retrieved from https:\/\/arxiv.org\/abs\/2404.05934"},{"key":"e_1_3_3_82_2","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying Li Zhou and Gilles Barthe. 2025. Laws of quantum programming. arXiv:2412.19463. Retrieved from https:\/\/arxiv.org\/abs\/2412.19463","DOI":"10.1145\/3765903"},{"key":"e_1_3_3_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3587154"},{"key":"e_1_3_3_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656397"},{"key":"e_1_3_3_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649811"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729283"},{"key":"e_1_3_3_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0165-3"},{"key":"e_1_3_3_89_2","first-page":"179","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL)","volume":"33","author":"Zuliani Paolo","year":"2004","unstructured":"Paolo Zuliani. 2004. Non-deterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL), Vol. 33, TUCS, 179\u2013195."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3765903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T14:47:34Z","timestamp":1781707654000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3765903"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,17]]},"references-count":88,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2026,7,31]]}},"alternative-id":["10.1145\/3765903"],"URL":"https:\/\/doi.org\/10.1145\/3765903","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,17]]},"assertion":[{"value":"2025-01-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-07-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}