{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:07:56Z","timestamp":1790075276779,"version":"4.0.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP250102952"],"award-info":[{"award-number":["DP250102952"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).<\/jats:p>","DOI":"10.1145\/3808273","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"656-680","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Recursively Defined Quantum Circuits"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"University of Technology Sydney, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7436-0426","authenticated-orcid":false,"given":"Zhicheng","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_1_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3776712"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi Sumit Gulwani and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV). 934\u2013950. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67 10.1007\/978-3-642-39799-8_67","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch and Jonathan Grattage. 2005. A Functional Quantum Programming Language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS). 249\u2013258. https:\/\/doi.org\/10.1109\/LICS.2005.1 10.1109\/LICS.2005.1","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90037-I"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2244643"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.195.3"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Benjamin Bichsel Maximilian Baader Timon Gehr and Martin T. Vechev. 2020. Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 286\u2013300. https:\/\/doi.org\/10.1145\/3385412.3386007 10.1145\/3385412.3386007","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632861"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90660-2_5"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3725728"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1965-0178586-1"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632901"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.87.217901"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/531340"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.59.1829"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/5.1.10"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00976239"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656436"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Mathieu Huot and Sam Staton. 2019. Quantum Channels as a Categorical Completion. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 35:1\u201335:13. https:\/\/doi.org\/10.1109\/LICS.2019.8785700 10.1109\/LICS.2019.8785700","DOI":"10.1109\/LICS.2019.8785700"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3406306"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_22"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-96753-4"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","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). 846\u2013858. https:\/\/doi.org\/10.1145\/3009837.3009894 10.1145\/3009837.3009894","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_29"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.113.130503"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_19"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.855930"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2015. Algebraic Effects Linearity and Quantum Programming Languages. In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL). 395\u2013406. https:\/\/doi.org\/10.1145\/2676726.2676999 10.1145\/2676726.2676999","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Runzhou Tao Yunong Shi Jianan Yao John Hui Frederic T. Chong and Ronghui Gu. 2021. Gleipnir: Toward Practical Error Analysis for Quantum Programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). 48\u201364. https:\/\/doi.org\/10.1145\/3453483.3454029 10.1145\/3453483.3454029","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_3_1_49_2","first-page":"1","article-title":"On Infinite Direct Products","volume":"6","author":"von Neumann John","year":"1939","unstructured":"John von Neumann. 1939. On Infinite Direct Products. Compositio Mathematica 6 (1939), 1\u201377.","journal-title":"Compositio Mathematica"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.109.050505"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"Zhaowei Xu Mingsheng Ying and Beno\u00eet Valiron. 2021. Reasoning about Recursive Quantum Programs. https:\/\/doi.org\/10.48550\/arXiv.2107.11679 10.48550\/arXiv.2107.11679 arXiv:2107.11679 [cs.LO]","DOI":"10.48550\/arXiv.2107.11679"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Mingsheng Ying. 2014. Quantum Recursion and Second Quantisation. https:\/\/doi.org\/10.48550\/arXiv.1405.4443 10.48550\/arXiv.1405.4443 arXiv:1405.4443 [quant-ph]","DOI":"10.48550\/arXiv.1405.4443"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/C2014-0-02660-3"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","unstructured":"Mingsheng Ying Nengkun Yu and Yuan Feng. 2012. Defining Quantum Control Flow. https:\/\/doi.org\/10.48550\/arXiv.1209.4379 10.48550\/arXiv.1209.4379 arXiv:1209.4379 [quant-ph]","DOI":"10.48550\/arXiv.1209.4379"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Mingsheng Ying and Zhicheng Zhang. 2024. Verification of Recursively Defined Quantum Circuits. https:\/\/doi.org\/10.48550\/arXiv.2404.05934 10.48550\/arXiv.2404.05934 arXiv:2404.05934 [quant-ph]","DOI":"10.48550\/arXiv.2404.05934"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563297"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649811"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","unstructured":"Li Zhou Nengkun Yu and Mingsheng Ying. 2019. An Applied Quantum Hoare Logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 1149\u20131162. https:\/\/doi.org\/10.1145\/3314221.3314584 10.1145\/3314221.3314584","DOI":"10.1145\/3314221.3314584"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808273","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:47:11Z","timestamp":1790074031000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808273"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":61,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808273"],"URL":"https:\/\/doi.org\/10.1145\/3808273","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}