{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T06:51:23Z","timestamp":1787727083989,"version":"build-2784847793"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100021130","name":"Bundesministerium f\u00fcr Wirtschaft und Klimaschutz","doi-asserted-by":"crossref","award":["01MQ22006F"],"award-info":[{"award-number":["01MQ22006F"]}],"id":[{"id":"10.13039\/100021130","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101040907"],"award-info":[{"award-number":["101040907"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["390781972"],"award-info":[{"award-number":["390781972"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["OCENW.KLEIN.267"],"award-info":[{"award-number":["OCENW.KLEIN.267"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002347","name":"Bundesministerium f\u00fcr Bildung und Forschung","doi-asserted-by":"publisher","award":["13N16135, 13N16303, 13N17173, 13N17170"],"award-info":[{"award-number":["13N16135, 13N16303, 13N17173, 13N17170"]}],"id":[{"id":"10.13039\/501100002347","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":[[2025,4,9]]},"abstract":"<jats:p>\n                    Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose\n                    <jats:italic toggle=\"yes\">Quantum Correctness by Construction (QbC)<\/jats:italic>\n                    : an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.\n                  <\/jats:p>","DOI":"10.1145\/3720433","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"534-562","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["QbC: Quantum Correctness by Construction"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6523-7098","authenticated-orcid":false,"given":"Anurudh","family":"Peduri","sequence":"first","affiliation":[{"name":"Ruhr University Bochum, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7153-761X","authenticated-orcid":false,"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"KIT, Karlsruhe, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3073-1408","authenticated-orcid":false,"given":"Michael","family":"Walter","sequence":"additional","affiliation":[{"name":"Ruhr University Bochum, Bochum, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/992287.992296"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_40"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ESA.2023.10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704876"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/248932"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_5"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591335.3591343"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/305\/05215"},{"key":"e_1_3_2_18_2","first-page":"31","article-title":"Foundations of the B Method","volume":"22","author":"Cansell Dominique","year":"2003","unstructured":"Dominique Cansell and Dominique Mery. 2003. Foundations of the B Method. Computers and Informatics 22 (01 2003), 31 p.","journal-title":"Computers and Informatics"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2023-04-27-988"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/780542.780552"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/2584504"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46674-6_11"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/550359"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_26_2","unstructured":"Yuan Feng Li Zhou and Yingte Xu. 2023. Refinement calculus of quantum programs with projective assertions. arXiv:2311.14215 [cs.LO]"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3313276.3316366"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.100.160501"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.l03.150502"},{"key":"e_1_3_2_33_2","unstructured":"HaskellWiki. 2014. GHC\/Typed holes \u2014 HaskellWiki. https:\/\/wiki.haskell.org\/index.php?title=GHC\/Typed_holes&oldid=58717 [Online; accessed 25-January-2024]."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_37_2","unstructured":"A. Yu. Kitaev. 1995. Quantum measurements and the Abelian Stabilizer Problem. arXiv:quant-ph\/9511026 [quant-ph] https:\/\/arxiv.org\/abs\/quant-ph\/9511026"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61362-4_10"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5"},{"key":"e_1_3_2_40_2","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. arXiv:2205.05781 [quant-ph] https:\/\/arxiv.org\/abs\/2205.05781"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.95.030505"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1103\/PRXQuantum.2.040203"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1038\/npjqi.2015.23"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_3_2_47_2","unstructured":"Carroll Morgan and Annabelle McIver. 1999. pGCL: Formal reasoning for random algorithms. South African Computer Journal 14\u201327."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3117515"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290327"},{"key":"e_1_3_2_53_2","first-page":"1277","article-title":"Repeat-until-success: non-deterministic decomposition of single-qubit unitaries","volume":"14","author":"Paetznick Adam","year":"2014","unstructured":"Adam Paetznick and Krysta M. Svore. 2014. Repeat-until-success: non-deterministic decomposition of single-qubit unitaries. Quantum Info. Comput. 14, 15\u201316 (nov 2014), 1277\u20131301.","journal-title":"Quantum Info. Comput."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_24"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_56_2","unstructured":"Robert Rand. 2019. Verification Logics for Quantum Programs. arXiv:1904.04304 [cs.LO]"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.287.17"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.266.8"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(2:16)2023"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391565"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08679-3_9"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_2"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_25"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747181"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_66_2","volume-title":"Quantum Correctness By Construction On The Web","author":"Seng Niklas","year":"2024","unstructured":"Niklas Seng. 2024. Quantum Correctness By Construction On The Web. Bachelor\u2019s thesis. Karlsruhe Institute of Technology. See http:\/\/qbc.kastel.kit.edu and also http:\/\/qbc.kastel.kit.edu\/tutorial."},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"P.W. Shor. 1994. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science. 124\u2013134. doi:10.1109\/SFCS.1994.365700","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_2_68_2","unstructured":"Jeremy Siek and Walid Taha. 2006. Gradual typing for functional languages. Scheme and Functional Programming."},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-01-31-49"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_20"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.110"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47166-2_52"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139525343"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704878"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813887"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563297"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","unstructured":"Paolo Zuliani. 2007. A Formal Derivation of Grover\u2019s Quantum Search Algorithm. In First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE \u201807). 67\u201374. doi:10.1109\/TASE.2007.3","DOI":"10.1109\/TASE.2007.3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720433","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720433","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:30:41Z","timestamp":1787589041000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720433"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":84,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720433"],"URL":"https:\/\/doi.org\/10.1145\/3720433","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}