{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:10Z","timestamp":1780994590599,"version":"3.54.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100011030","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["FOA?18?1895, DE-SC0019040"],"award-info":[{"award-number":["FOA?18?1895, DE-SC0019040"]}],"id":[{"id":"10.13039\/100011030","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007631","name":"Canadian Institute for Advanced Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100007631","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":[[2019,1,2]]},"abstract":"<jats:p>Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called \u0454-robustness, which characterizes possible \u201cdistance\u201d between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.<\/jats:p>","DOI":"10.1145\/3290344","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Quantitative robustness analysis of quantum programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Shih-Han","family":"Hung","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kesha","family":"Hietala","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaopeng","family":"Zhu","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia \/ Institute of Software at Chinese Academy of Sciences, China \/ Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaodi","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Fred Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun.","author":"Abhari Ali Javadi","year":"2012","unstructured":"Ali Javadi Abhari , Arvin Faruque , Mohammad Javad Dousti , Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Fred Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. 2012 . Scaffold : Quantum Programming Language. Technical Report TR-934-12. Princeton University . Ali Javadi Abhari, Arvin Faruque, Mohammad Javad Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Fred Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. 2012. Scaffold: Quantum Programming Language. Technical Report TR-934-12. Princeton University."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380758"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/258533.258579"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806620"},{"key":"e_1_2_2_5_1","volume-title":"Quantum Logic as a Dynamic Logic. Synthese 179, 2","author":"Baltag Alexandru","year":"2011","unstructured":"Alexandru Baltag and Sonja Smets . 2011. Quantum Logic as a Dynamic Logic. Synthese 179, 2 ( 2011 ). Alexandru Baltag and Sonja Smets. 2011. Quantum Logic as a Dynamic Logic. Synthese 179, 2 (2011)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541958"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814301"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254086"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_2_2_14_1","volume-title":"Programming Languages and Compiler Design for Realistic Quantum Hardware. Nature 549","author":"Chong Frederic T.","year":"2017","unstructured":"Frederic T. Chong , Diana Franklin , and Margaret Martonosi . 2017. Programming Languages and Compiler Design for Realistic Quantum Hardware. Nature 549 ( 2017 ). Frederic T. Chong, Diana Franklin, and Margaret Martonosi. 2017. Programming Languages and Compiler Design for Realistic Quantum Hardware. Nature 549 (2017)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1080\/09500349708231894"},{"key":"e_1_2_2_16_1","unstructured":"Marcus P. da Silva. 2015. matlab-diamond-norm: A MATLAB function for computing the diamond norm (completely bounded induced 1-norm on linear superoperators). https:\/\/github.com\/BBN- Q\/matlab- diamond- norm  Marcus P. da Silva. 2015. matlab-diamond-norm: A MATLAB function for computing the diamond norm (completely bounded induced 1-norm on linear superoperators). https:\/\/github.com\/BBN- Q\/matlab- diamond- norm"},{"key":"e_1_2_2_17_1","volume-title":"Provable Quantum Advantage in Randomness Processing. Nature Communications 6","author":"Dale Howard","year":"2015","unstructured":"Howard Dale , David Jennings , and Terry Rudolph . 2015. Provable Quantum Advantage in Randomness Processing. Nature Communications 6 ( 2015 ). Howard Dale, David Jennings, and Terry Rudolph. 2015. Provable Quantum Advantage in Randomness Processing. Nature Communications 6 (2015)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1088\/1464-4266\/7\/10\/021"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.032324"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.86.153"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.71.062310"},{"key":"e_1_2_2_25_1","volume-title":"Proceedings of Symposia in Applied Mathematics: Quantum Information Science and Its Contributions to Mathematics 68","author":"Gottesman Daniel","year":"2010","unstructured":"Daniel Gottesman . 2010 . An Introduction to Quantum Error Correction and Fault-tolerant Quantum Computation . Proceedings of Symposia in Applied Mathematics: Quantum Information Science and Its Contributions to Mathematics 68 (2010). Daniel Gottesman. 2010. An Introduction to Quantum Error Correction and Fault-tolerant Quantum Computation. Proceedings of Symposia in Applied Mathematics: Quantum Information Science and Its Contributions to Mathematics 68 (2010)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.87.030302"},{"key":"e_1_2_2_29_1","volume-title":"Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585","author":"Hung Shih-Han","year":"2018","unstructured":"Shih-Han Hung , Kesha Hietala , Shaopeng Zhu , Mingsheng Ying , Michael Hicks , and Xiaodi Wu. 2018. Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585 ( 2018 ). arXiv: 1811.03585 Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. 2018. Quantitative Robustness Analysis of Quantum Programs (Extended Version). CoRR abs\/1811.03585 (2018). arXiv: 1811.03585"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/175007.175019"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.77.012307"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158123"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.106.180504"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660231"},{"key":"e_1_2_2_36_1","volume-title":"Quantum Optimization Using Variational Algorithms on Near-term Quantum Devices. Quantum Science and Technology 3, 3","author":"Moll Nikolaj","year":"2018","unstructured":"Nikolaj Moll , Panagiotis Barkoutsos , Lev S. Bishop , Jerry M. Chow , Andrew Cross , Daniel J. Egger , Stefan Filipp , Andreas Fuhrer , Jay M. Gambetta , Marc Ganzhorn , Abhinav Kandala , Antonio Mezzacapo , Peter M\u00fcller , Walter Riess , Gian Salis , John Smolin , Ivano Tavernelli , and Kristan Temme . 2018. Quantum Optimization Using Variational Algorithms on Near-term Quantum Devices. Quantum Science and Technology 3, 3 ( 2018 ). Nikolaj Moll, Panagiotis Barkoutsos, Lev S. Bishop, Jerry M. Chow, Andrew Cross, Daniel J. Egger, Stefan Filipp, Andreas Fuhrer, Jay M. Gambetta, Marc Ganzhorn, Abhinav Kandala, Antonio Mezzacapo, Peter M\u00fcller, Walter Riess, Gian Salis, John Smolin, Ivano Tavernelli, and Kristan Temme. 2018. Quantum Optimization Using Variational Algorithms on Near-term Quantum Devices. Quantum Science and Technology 3, 3 (2018)."},{"key":"e_1_2_2_37_1","volume-title":"Nielsen and Isaac Chuang","author":"Michael","year":"2000","unstructured":"Michael A. Nielsen and Isaac Chuang . 2000 . Quantum Computation and Quantum Information. Cambridge University Press . Michael A. Nielsen and Isaac Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786807"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250741"},{"key":"e_1_2_2_42_1","volume-title":"O\u2019Brien","author":"Peruzzo Alberto","year":"2014","unstructured":"Alberto Peruzzo , Jarrod McClean , Peter Shadbolt , Man-Hong Yung , Xiao-Qi Zhou , Peter J. Love , Al\u00e1n Aspuru-Guzik , and Jeremy L . O\u2019Brien . 2014 . A Variational Eigenvalue Solver on a Photonic Quantum Processor. Nature Communications 5, 4213 (2014). Alberto Peruzzo, Jarrod McClean, Peter Shadbolt, Man-Hong Yung, Xiao-Qi Zhou, Peter J. Love, Al\u00e1n Aspuru-Guzik, and Jeremy L. O\u2019Brien. 2014. A Variational Eigenvalue Solver on a Photonic Quantum Processor. Nature Communications 5, 4213 (2014)."},{"key":"e_1_2_2_43_1","volume-title":"Quantum Computing in the NISQ Era and Beyond. Quantum 2, 79","author":"Preskill John","year":"2018","unstructured":"John Preskill . 2018. Quantum Computing in the NISQ Era and Beyond. Quantum 2, 79 ( 2018 ). John Preskill. 2018. Quantum Computing in the NISQ Era and Beyond. Quantum 2, 79 (2018)."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/871895.871900"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993518"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594294"},{"key":"e_1_2_2_47_1","volume-title":"Sanders and Paolo Zuliani","author":"Jeff","year":"2000","unstructured":"Jeff W. Sanders and Paolo Zuliani . 2000 . Quantum Programming. In MPC. Jeff W. Sanders and Paolo Zuliani. 2000. Quantum Programming. In MPC."},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Peter Selinger. 2004a. A Brief Survey of Quantum Programming Languages. In FLOPS.  Peter Selinger. 2004a. A Brief Survey of Quantum Programming Languages. In FLOPS.","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Martin Suchara John Kubiatowicz Arvin I. Faruque Frederic T. Chong Ching-Yi Lai and Gerardo Paz. 2013. QuRE: The Quantum Resource Estimator Toolbox. In ICCD.  Martin Suchara John Kubiatowicz Arvin I. Faruque Frederic T. Chong Ching-Yi Lai and Gerardo Paz. 2013. QuRE: The Quantum Resource Estimator Toolbox. In ICCD.","DOI":"10.1109\/ICCD.2013.6657074"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.87.307"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159809"},{"key":"e_1_2_2_54_1","unstructured":"John Watrous. 2006. Introduction to Quantum Computation. https:\/\/cs.uwaterloo.ca\/~watrous\/LectureNotes\/CPSC519. Winter2006\/all.pdf . Course notes.  John Watrous. 2006. Introduction to Quantum Computation. https:\/\/cs.uwaterloo.ca\/~watrous\/LectureNotes\/CPSC519. Winter2006\/all.pdf . Course notes."},{"key":"e_1_2_2_55_1","volume-title":"Semidefinite Programs for Completely Bounded Norms. Theory of Computing 5, 11","author":"Watrous John","year":"2009","unstructured":"John Watrous . 2009. Semidefinite Programs for Completely Bounded Norms. Theory of Computing 5, 11 ( 2009 ). John Watrous. 2009. Semidefinite Programs for Completely Bounded Norms. Theory of Computing 5, 11 (2009)."},{"key":"e_1_2_2_56_1","article-title":"Simpler Semidefinite Programs for Completely Bounded Norms","volume":"2013","author":"Watrous John","year":"2013","unstructured":"John Watrous . 2013 . Simpler Semidefinite Programs for Completely Bounded Norms . Chicago Journal of Theoretical Computer Science 2013 , 8 (2013). John Watrous. 2013. Simpler Semidefinite Programs for Completely Bounded Norms. Chicago Journal of Theoretical Computer Science 2013, 8 (2013).","journal-title":"Chicago Journal of Theoretical Computer Science"},{"key":"e_1_2_2_57_1","volume-title":"The Theory of Quantum Information","author":"Watrous John","unstructured":"John Watrous . 2018. The Theory of Quantum Information . Cambridge University Press . John Watrous. 2018. The Theory of Quantum Information. Cambridge University Press."},{"key":"e_1_2_2_58_1","volume-title":"A Software Design Architecture and Domain-Specific Language for Quantum Computing. CoRR abs\/1402.4467","author":"Wecker Dave","year":"2014","unstructured":"Dave Wecker and Krysta Svore . 2014. LIQ Ui |\u27e9 : A Software Design Architecture and Domain-Specific Language for Quantum Computing. CoRR abs\/1402.4467 ( 2014 ). arXiv: 1402.4467 Dave Wecker and Krysta Svore. 2014. LIQUi |\u27e9: A Software Design Architecture and Domain-Specific Language for Quantum Computing. CoRR abs\/1402.4467 (2014). arXiv: 1402.4467"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.   Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009840"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290344","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290344","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290344"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290344"],"URL":"https:\/\/doi.org\/10.1145\/3290344","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}