{"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":1785290933746,"version":"3.55.0"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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\n                    <jats:italic toggle=\"yes\">assertion language<\/jats:italic>\n                    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\n                    <jats:italic toggle=\"yes\">expressive<\/jats:italic>\n                    with respect to the quantum programs with loops\u2013specifically, for any program\n                    <jats:italic toggle=\"yes\">S<\/jats:italic>\n                    and any postcondition\n                    <jats:italic toggle=\"yes\">\u03c8<\/jats:italic>\n                    formulated in the assertion language, the\n                    <jats:italic toggle=\"yes\">weakest precondition<\/jats:italic>\n                    of\n                    <jats:italic toggle=\"yes\">S<\/jats:italic>\n                    with respect to\n                    <jats:italic toggle=\"yes\">\u03c8<\/jats:italic>\n                    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":1,"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_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.384.8"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704876"},{"key":"e_1_3_2_6_2","volume-title":"Mathematical Theory of Program Correctness","author":"de Bakker J. W.","year":"1980","unstructured":"J. W. de Bakker. 1980. Mathematical Theory of Program Correctness. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Minbo Gao Theo Wang and Li Zhou. 2025. Complete Quantum Relational Hoare Logics from Optimal Transport Duality. arXiv:2501.15238 [cs.LO] https:\/\/arxiv.org\/abs\/2501.15238","DOI":"10.1109\/LICS65433.2025.00072"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656430"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.95.045005"},{"issue":"84","key":"e_1_3_2_14_2","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_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-3-031-37709-9_7","volume-title":"Computer Aided Verification","author":"Chen Yu-Fang","year":"2023","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."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_2_19_2","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_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/322108.322121"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_11"},{"key":"e_1_3_2_26_2","unstructured":"Ellie D\u2019Hondt and Prakash Panangaden. 2006. Quantum Weakest Preconditions. arXiv:quant-ph\/0501157 [quant-ph] https:\/\/arxiv.org\/abs\/quant-ph\/0501157"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/550359"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.111.042619"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Yuan Feng Li Zhou Yingte Xu and Xiaoquan Xu. 2025. Refinement calculus of quantum programs with projective assertions. ACM Trans. Softw. Eng. Methodol. (Oct. 2025). https:\/\/doi.org\/10.1145\/3770083 10.1145\/3770083 Just Accepted.","DOI":"10.1145\/3770083"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01700692"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729293"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_39_2","first-page":"11","article-title":"New directions in categorical logic, for classical, probabilistic and quantum logic","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).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209131"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.14"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12732-1"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_2_48_2","unstructured":"Adrian Lehmann Ben Caldwell Bhakti Shah and Robert Rand. 2023. VyZX: Formal Verification of a Graphical Quantum Language. arXiv:2311.11571 [cs.PL] https:\/\/arxiv.org\/abs\/2311.11571"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571198"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158123"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.5555\/1036296"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_24"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3720433"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523713"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"Qiskit contributors. 2023. Qiskit: An Open-source Framework for Quantum Computing. https:\/\/doi.org\/10.5281\/zenodo.2573505 10.5281\/zenodo.2573505","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.340.14"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266510"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.384.9"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676999"},{"key":"e_1_3_2_67_2","unstructured":"Aarthi Sundaram Robert Rand Kartik Singhal and Brad Lackey. 2025. Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. arXiv:2101.08939 [quant-ph] https:\/\/arxiv.org\/abs\/2101.08939"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_71_2","first-page":"13","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (Vancouver, Canada) (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 (Vancouver, Canada) (LICS \u201919). IEEE Press, Article 47, 13 pages."},{"key":"e_1_3_2_72_2","unstructured":"John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] https:\/\/arxiv.org\/abs\/2012.13966"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/14\/11\/113011"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_3_2_75_2","volume-title":"Completeness of the ZX-calculus. Ph. D. Dissertation","author":"Wang Quanlong","year":"2018","unstructured":"Quanlong Wang. 2018. Completeness of the ZX-calculus. Ph. D. Dissertation. Oxford U. arXiv:2209.14894 [quant-ph]"},{"key":"e_1_3_2_76_2","unstructured":"Dave Wecker and Krysta M. Svore. 2014. LIQUi\u013c>: A Software Design Architecture and Domain-Specific Language for Quantum Computing. arXiv:1402.4467 [quant-ph] https:\/\/arxiv.org\/abs\/1402.4467"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_2_78_2","article-title":"QECV: Quantum Error Correction Verification","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 (2021).","journal-title":"arXiv preprint arXiv:2111.13728"},{"key":"e_1_3_2_79_2","unstructured":"Zhaowei Xu Mingsheng Ying and Beno\u00eet Valiron. 2021. Reasoning about Recursive Quantum Programs. arXiv:2107.11679 [cs.LO] https:\/\/arxiv.org\/abs\/2107.11679"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_81_2","article-title":"Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs","author":"Ying Mingsheng","year":"2022","unstructured":"Mingsheng Ying. 2022. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs. (5 2022). arXiv:2205.01959 [cs.LO]","journal-title":"arXiv:2205.01959 [cs.LO]"},{"key":"e_1_3_2_82_2","unstructured":"Mingsheng Ying. 2022. Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs. arXiv:2205.01959 [cs.LO] https:\/\/arxiv.org\/abs\/2205.01959"},{"key":"e_1_3_2_83_2","volume-title":"Foundations of quantum programming","author":"Ying Mingsheng","year":"2024","unstructured":"Mingsheng Ying. 2024. Foundations of quantum programming. Elsevier."},{"key":"e_1_3_2_84_2","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2024. A Practical Quantum Hoare Logic with Classical Variables I. arXiv:2412.09869 [cs.PL] https:\/\/arxiv.org\/abs\/2412.09869","DOI":"10.2139\/ssrn.5193712"},{"key":"e_1_3_2_85_2","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_3_2_86_2","doi-asserted-by":"crossref","first-page":"v","DOI":"10.1017\/9781108613323","volume-title":"Model Checking Quantum Systems: Principles and Algorithms","author":"Ying Mingsheng","year":"2021","unstructured":"Mingsheng Ying and Yuan Feng. 2021. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, v\u2013viii."},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2024.105197"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_2_91_2","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,7,16]],"date-time":"2026-07-16T13:39:44Z","timestamp":1784209184000},"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"}}]}}