{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:11:42Z","timestamp":1765667502338,"version":"3.41.2"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"abstract":"<jats:p>\n            We study\n            <jats:italic>expected runtimes<\/jats:italic>\n            for quantum programs. Inspired by recent work on probabilistic programs, we first define\n            <jats:italic>expected runtime<\/jats:italic>\n            as a generalisation of\n            <jats:italic>quantum weakest precondition<\/jats:italic>\n            . Then, we show that the expected runtime of a quantum program should be represented as the expectation of an\n            <jats:italic>observable<\/jats:italic>\n            (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory \u2013 a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et\u00a0al. (\n            <jats:italic>STOC<\/jats:italic>\n            2001) is solved.\n          <\/jats:p>","DOI":"10.1145\/3734516","type":"journal-article","created":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T11:35:41Z","timestamp":1746531341000},"update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5715-4885","authenticated-orcid":false,"given":"Junyi","family":"Liu","sequence":"first","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences,  Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences,  Beijing China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute,  Boadilla del Monte, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Tsinghua University, Beijing China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,5,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380758"},{"key":"e_1_2_1_2_1","unstructured":"Andris Ambainis. 2003. Quantum walk algorithm for element distinctness. arXiv preprint quant-ph\/0311001(2003)."},{"key":"e_1_2_1_3_1","volume-title":"International Conference on Current Trends in Theory and Practice of Computer Science. Springer, 1\u20134.","author":"Ambainis Andris","year":"2008","unstructured":"Andris Ambainis. 2008. Quantum random walks\u2013new method for designing quantum algorithms. In International Conference on Current Trends in Theory and Practice of Computer Science. Springer, 1\u20134."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380757"},{"key":"e_1_2_1_5_1","volume-title":"et\u00a0al","author":"Arute Frank","year":"2019","unstructured":"Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph\u00a0C Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando\u00a0GSL Brandao, David\u00a0A Buell, et\u00a0al. 2019. Quantum supremacy using a programmable superconducting processor. Nature 574, 7779 (2019), 505\u2013510."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533332"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_6"},{"key":"e_1_2_1_14_1","volume-title":"Quantum startup Atom Computing first to exceed 1,000 qubits. https:\/\/atom-computing.com\/quantum-startup-atom-computing-first-to-exceed-1000-qubits\/. Online","author":"Computing Atom","year":"2023","unstructured":"Atom Computing. 2023. Quantum startup Atom Computing first to exceed 1,000 qubits. https:\/\/atom-computing.com\/quantum-startup-atom-computing-first-to-exceed-1000-qubits\/. Online; accessed 27-Dec-2023."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Howard Dale David Jennings and Terry Rudolph. 2015. Provable quantum advantage in randomness processing. Nature communications 6(2015) 8203.","DOI":"10.1038\/ncomms9203"},{"key":"e_1_2_1_17_1","volume-title":"2017 IEEE Symposium on Security and Privacy (SP). IEEE, 710\u2013728","author":"Dehesa-Azuara Mario","year":"2017","unstructured":"Mario Dehesa-Azuara, Matthew Fredrikson, Jan Hoffmann, et\u00a0al. 2017. Verifying and synthesizing constant-resource implementations with types. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE, 710\u2013728."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_20_1","volume-title":"The hardware and software for the era of quantum utility is here. https:\/\/www.ibm.com\/quantum\/blog\/quantum-roadmap-2033. Online","author":"Gambetta Jay","year":"2023","unstructured":"Jay Gambetta. 2023. The hardware and software for the era of quantum utility is here. https:\/\/www.ibm.com\/quantum\/blog\/quantum-roadmap-2033. Online; accessed 27-Dec-2023."},{"key":"e_1_2_1_21_1","volume-title":"et\u00a0al","author":"Gong Ming","year":"2021","unstructured":"Ming Gong, Shiyu Wang, Chen Zha, Ming-Cheng Chen, He-Liang Huang, Yulin Wu, Qingling Zhu, Youwei Zhao, Shaowei Li, Shaojun Guo, et\u00a0al. 2021. Quantum walks on a programmable two-dimensional 62-qubit superconducting processor. Science 372, 6545 (2021), 948\u2013952."},{"key":"e_1_2_1_22_1","volume-title":"Type-based amortized resource analysis with integers and arrays. Journal of Functional Programming 25","author":"Hoffmann Jan","year":"2015","unstructured":"Jan Hoffmann and Zhong Shao. 2015. Type-based amortized resource analysis with integers and arrays. Journal of Functional Programming 25 (2015)."},{"key":"e_1_2_1_23_1","volume-title":"13th International Conference on Typed Lambda Calculi and Applications (TLCA","author":"Hofmann Martin","year":"2015","unstructured":"Martin Hofmann and Georg Moser. 2015. Multivariate amortised resource analysis for term rewrite systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"volume-title":"Matrix analysis","author":"Horn A","key":"e_1_2_1_24_1","unstructured":"Roger\u00a0A Horn and Charles\u00a0R Johnson. 2012. Matrix analysis. Cambridge university press."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Ali JavadiAbhari Shruti Patil Daniel Kudrow Jeff Heckey Alexey Lvov Fredric T.Chong and Margaret Martonosi. 2015. ScaffCC: Scalable compilation and analysis of quantum programs. In Parallel Computing 45. 3\u201317.","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-018-2017-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533327"},{"volume-title":"refinement and proof for probabilistic systems","author":"McIver Annabelle","key":"e_1_2_1_30_1","unstructured":"Annabelle McIver, Carroll Morgan, and Charles\u00a0Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Van\u00a0Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In ACM SIGPLAN Notices Vol.\u00a0 53. ACM 496\u2013512.","DOI":"10.1145\/3296979.3192394"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Michael\u00a0A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information.","DOI":"10.1119\/1.1463744"},{"key":"e_1_2_1_33_1","unstructured":"Federico Olmedo and Alejandro D\u00edaz-Caro. 2019. Runtime Analysis of Quantum Programs: A Formal Approach. arXiv preprint arXiv:1911.11247(2019)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70697-9_9"},{"key":"e_1_2_1_37_1","volume-title":"Quantum Programming. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000)","author":"Sanders J.","year":"1837","unstructured":"J. Sanders and P. Zuliani. 2000. Quantum Programming. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000)(LNCS, Vol.\u00a0 1837). 80\u201399."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.67.052307"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.94"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009840"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3734516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T11:35:48Z","timestamp":1746531348000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3734516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,6]]},"references-count":46,"alternative-id":["10.1145\/3734516"],"URL":"https:\/\/doi.org\/10.1145\/3734516","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2025,5,6]]},"assertion":[{"value":"2022-12-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-16","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-05-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3734516"}}