{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T15:53:19Z","timestamp":1781711599920,"version":"3.54.5"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"name":"Quantum Science and Technology-National Science and Technology Major Project","award":["2024ZD0300500"],"award-info":[{"award-number":["2024ZD0300500"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["92465202"],"award-info":[{"award-number":["92465202"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012401","name":"Beijing Science and Technology Planning Project","doi-asserted-by":"crossref","award":["Z25110100810000"],"award-info":[{"award-number":["Z25110100810000"]}],"id":[{"id":"10.13039\/501100012401","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques such as G\u00f6delization to prove that this language is expressive with respect to the quantum programs with loops\u2014specifically, for any program\n                    <jats:italic toggle=\"yes\">S<\/jats:italic>\n                    and any postcondition \u03c8 formulated in the assertion language, the weakest precondition of\n                    <jats:italic toggle=\"yes\">S<\/jats:italic>\n                    with respect to \u03c8 can also be expressed as a formula in the assertion language. As an application, we present a sound and relatively complete quantum Hoare logic upon our expressive assertion language.\n                  <\/jats:p>","DOI":"10.1145\/3776658","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"444-475","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Expressive Assertion Language for Quantum Programs"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-7279-0658","authenticated-orcid":false,"given":"Bonan","family":"Su","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3097-3896","authenticated-orcid":false,"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"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":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.384.8"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704876"},{"key":"e_1_2_2_5_1","volume-title":"Mathematical Theory of Program Correctness","author":"de Bakker J. W.","unstructured":"J. W. de Bakker. 1980. Mathematical Theory of Program Correctness. Prentice-Hall, Inc., USA. isbn:0135621321"},{"key":"e_1_2_2_6_1","unstructured":"Gilles Barthe Minbo Gao Theo Wang and Li Zhou. 2025. Complete Quantum Relational Hoare Logics from Optimal Transport Duality. arxiv:2501.15238. arxiv:2501.15238"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656430"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.95.045005"},{"key":"e_1_2_2_13_1","first-page":"242","article-title":"Ein beitrag zur mannigfaltigkeitslehre","volume":"1878","author":"Cantor Georg","year":"1878","unstructured":"Georg Cantor. 1878. Ein beitrag zur mannigfaltigkeitslehre. Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal), 1878, 84 (1878), 242\u2013258.","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal)"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_2_15_1","volume-title":"Beno\u00eet Valiron, Renaud Vilmart, and Zhaowei Xu.","author":"Chareton Christophe","year":"2023","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. https:\/\/cea.hal.science\/cea-04479879"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen Kai-Min Chung Ond\u0159ej Leng\u00e1l Jyun-Ao Lin and Wei-Lun Tsai. 2023. AutoQ: An Automata-Based Quantum Circuit Verifier. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 139\u2013153. isbn:978-3-031-37709-9","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2023. Cirq. https:\/\/doi.org\/10.5281\/zenodo.8161252 10.5281\/zenodo.8161252","DOI":"10.5281\/zenodo.8161252"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/322108.322121"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_11"},{"key":"e_1_2_2_25_1","unstructured":"Ellie D\u2019Hondt and Prakash Panangaden. 2006. Quantum Weakest Preconditions. arxiv:quant-ph\/0501157. arxiv:quant-ph\/0501157"},{"key":"e_1_2_2_26_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","unstructured":"Edsger Wybe Dijkstra. 1997. A Discipline of Programming (1st ed.). Prentice Hall PTR, USA. isbn:013215871X","edition":"1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.111.042619"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3770083"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729293"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_2_2_38_1","volume-title":"New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, 11","author":"Jacobs Bart","year":"2015","unstructured":"Bart Jacobs. 2015. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, 11 (2015)."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209131"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12732-1"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_2_2_47_1","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. arxiv:2311.11571. arxiv:2311.11571"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571198"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158123"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_2_2_54_1","volume-title":"Refinement And Proof For Probabilistic Systems (Monographs in Computer Science)","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). SpringerVerlag. isbn:0387401156"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_24"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720433"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523713"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.340.14"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266510"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.384.9"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676999"},{"key":"e_1_2_2_66_1","unstructured":"Aarthi Sundaram Robert Rand Kartik Singhal and Brad Lackey. 2025. Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. arxiv:2101.08939. arxiv:2101.08939"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_2_70_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Unruh Dominique","year":"2021","unstructured":"Dominique Unruh. 2021. Quantum Hoare logic with ghost variables. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE Press, Article 47, 13 pages."},{"key":"e_1_2_2_71_1","unstructured":"John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arxiv:2012.13966. arxiv:2012.13966"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/14\/11\/113011"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_2_2_74_1","unstructured":"Quanlong Wang. 2018. Completeness of the ZX-calculus. Ph. D. Dissertation. Oxford U.. arxiv:2209.14894."},{"key":"e_1_2_2_75_1","volume-title":"Svore","author":"Wecker Dave","year":"2014","unstructured":"Dave Wecker and Krysta M. Svore. 2014. LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing. arxiv:1402.4467. arxiv:1402.4467"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"},{"key":"e_1_2_2_77_1","volume-title":"Yuan Xie, and Yufei Ding.","author":"Wu Anbang","year":"2021","unstructured":"Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding. 2021. QECV: Quantum Error Correction Verification. arXiv preprint arXiv:2111.13728."},{"key":"e_1_2_2_78_1","unstructured":"Zhaowei Xu Mingsheng Ying and Beno\u00eet Valiron. 2021. Reasoning about Recursive Quantum Programs. arxiv:2107.11679. arxiv:2107.11679"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_80_1","unstructured":"Mingsheng Ying. 2022. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs. 5 arxiv:2205.01959."},{"key":"e_1_2_2_81_1","unstructured":"Mingsheng Ying. 2022. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs. arxiv:2205.01959. arxiv:2205.01959"},{"key":"e_1_2_2_82_1","volume-title":"Foundations of quantum programming","author":"Ying Mingsheng","unstructured":"Mingsheng Ying. 2024. Foundations of quantum programming. Elsevier."},{"key":"e_1_2_2_83_1","unstructured":"Mingsheng Ying. 2024. A Practical Quantum Hoare Logic with Classical Variables I. arxiv:2412.09869. arxiv:2412.09869"},{"key":"e_1_2_2_84_1","first-page":"311","article-title":"Predicate transformer semantics of quantum programs","volume":"8","author":"Ying MS","year":"2010","unstructured":"MS Ying, RY Duan, Yuan Feng, and ZF Ji. 2010. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation, 8 (2010), 311\u2013360.","journal-title":"Semantic Techniques in Quantum Computation"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108613323"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2024.105197"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776658","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T15:13:10Z","timestamp":1781709190000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776658"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":90,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776658"],"URL":"https:\/\/doi.org\/10.1145\/3776658","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}