{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T13:11:25Z","timestamp":1774703485251,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,3,25]],"date-time":"2023-03-25T00:00:00Z","timestamp":1679702400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP220102059"],"award-info":[{"award-number":["DP220102059"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,3,25]]},"DOI":"10.1145\/3582016.3582039","type":"proceedings-article","created":{"date-parts":[[2023,3,20]],"date-time":"2023-03-20T16:59:03Z","timestamp":1679331543000},"page":"789-805","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verification of Nondeterministic Quantum Programs"],"prefix":"10.1145","author":[{"given":"Yuan","family":"Feng","sequence":"first","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingte","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,3,25]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Refinement calculus: a systematic introduction","author":"Back Ralph-Johan","unstructured":"Ralph-Johan Back and Joakim Wright . 2012. Refinement calculus: a systematic introduction . Springer Science & Business Media . Ralph-Johan Back and Joakim Wright. 2012. Refinement calculus: a systematic introduction. Springer Science & Business Media."},{"key":"e_1_3_2_1_2_1","volume-title":"On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory. 427\u2013440","author":"Deng Yuxin","year":"2015","unstructured":"Yuxin Deng , Yuan Feng , and Ugo Dal Lago . 2015 . On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory. 427\u2013440 . Yuxin Deng, Yuan Feng, and Ugo Dal Lago. 2015. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory. 427\u2013440."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences, 400","author":"Deutsch David","year":"1985","unstructured":"David Deutsch . 1985 . Quantum theory, the Church\u2013Turing principle and the universal quantum computer . Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences, 400 , 1818 (1985), 97\u2013117. David Deutsch. 1985. Quantum theory, the Church\u2013Turing principle and the universal quantum computer. Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences, 400, 1818 (1985), 97\u2013117."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_1_5_1","volume-title":"A discipline of programming","author":"Dijkstra Edsger Wybe","unstructured":"Edsger Wybe Dijkstra . 1976. A discipline of programming . Prentice-Hall Englewood Cliffs . Edsger Wybe Dijkstra. 1976. A discipline of programming. Prentice-Hall Englewood Cliffs."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/S0167-6423(96)00019-6","article-title":"Probabilistic models for the guarded command language","volume":"28","author":"He Jifeng","year":"1997","unstructured":"Jifeng He , Karen Seidel , and Annabelle McIver . 1997 . Probabilistic models for the guarded command language . Science of Computer Programming , 28 , 2 - 3 (1997), 171\u2013192. Jifeng He, Karen Seidel, and Annabelle McIver. 1997. Probabilistic models for the guarded command language. Science of Computer Programming, 28, 2-3 (1997), 171\u2013192.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_1_9_1","volume-title":"Normal form approach to compiler design. Acta informatica, 30, 8","author":"Richard Hoare Charles Antony","year":"1993","unstructured":"Charles Antony Richard Hoare , He Jifeng , and Augusto Sampaio . 1993. Normal form approach to compiler design. Acta informatica, 30, 8 ( 1993 ), 701\u2013739. Charles Antony Richard Hoare, He Jifeng, and Augusto Sampaio. 1993. Normal form approach to compiler design. Acta informatica, 30, 8 (1993), 701\u2013739."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-12732-1","volume-title":"States, effects, and operations: fundamental notions of quantum theory. Lecture notes in physics, 190","author":"Kraus Karl","year":"1983","unstructured":"Karl Kraus , Arno B\u00f6hm , John D Dollard , and WH Wootters . 1983. States, effects, and operations: fundamental notions of quantum theory. Lecture notes in physics, 190 ( 1983 ). Karl Kraus, Arno B\u00f6hm, John D Dollard, and WH Wootters. 1983. States, effects, and operations: fundamental notions of quantum theory. Lecture notes in physics, 190 (1983)."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the ACM on Programming Languages. ACM New York, NY, USA, 1\u201329","author":"Li Yangjia","year":"2017","unstructured":"Yangjia Li and Mingsheng Ying . 2017 . Algorithmic analysis of termination problems for quantum programs . In Proceedings of the ACM on Programming Languages. ACM New York, NY, USA, 1\u201329 . Yangjia Li and Mingsheng Ying. 2017. Algorithmic analysis of termination problems for quantum programs. In Proceedings of the ACM on Programming Languages. ACM New York, NY, USA, 1\u201329."},{"key":"e_1_3_2_1_12_1","volume-title":"Termination of nondeterministic quantum programs. Acta informatica, 51, 1","author":"Li Yangjia","year":"2014","unstructured":"Yangjia Li , Nengkun Yu , and Mingsheng Ying . 2014. Termination of nondeterministic quantum programs. Acta informatica, 51, 1 ( 2014 ), 1\u201324. Yangjia Li, Nengkun Yu, and Mingsheng Ying. 2014. Termination of nondeterministic quantum programs. Acta informatica, 51, 1 (2014), 1\u201324."},{"key":"e_1_3_2_1_13_1","volume-title":"Formal Verification of Quantum Algorithms Using Quantum Hoare Logic","author":"Liu Junyi","unstructured":"Junyi Liu , Bohua Zhan , Shuling Wang , Shenggang Ying , Tao Liu , Yangjia Li , Mingsheng Ying , and Naijun Zhan . 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic . Springer , Cham , 187\u2013207. https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-25543-5_12 Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. Springer, Cham, 187\u2013207. https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0304-3975(00)00208-5"},{"key":"e_1_3_2_1_15_1","volume-title":"refinement and proof for probabilistic systems","author":"McIver Annabelle","unstructured":"Annabelle McIver , Carroll Morgan , and Charles Carroll Morgan . 2005. Abstraction , refinement and proof for probabilistic systems . Springer Science & Business Media . Annabelle McIver, Carroll Morgan, and Charles Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2000.0714"},{"key":"e_1_3_2_1_17_1","volume-title":"Program Design Calculi","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1993. The refinement calculus . In Program Design Calculi . Springer , 3\u201352. Carroll Morgan. 1993. The refinement calculus. In Program Design Calculi. Springer, 3\u201352."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_3_2_1_19_1","volume-title":"A theoretical basis for stepwise refinement and the programming calculus. Science of Computer programming, 9, 3","author":"Morris Joseph M","year":"1987","unstructured":"Joseph M Morris . 1987. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer programming, 9, 3 ( 1987 ), 287\u2013306. Joseph M Morris. 1987. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer programming, 9, 3 (1987), 287\u2013306."},{"key":"e_1_3_2_1_20_1","volume-title":"Quantum computation and quantum information","author":"Nielsen Michael A","unstructured":"Michael A Nielsen and Isaac Chuang . 2002. Quantum computation and quantum information . Cambridge University Press . Michael A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information. Cambridge University Press."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_3_2_1_22_1","volume-title":"International Conference on Mathematics of Program Construction. 80\u201399","author":"Sanders Jeff W","year":"2000","unstructured":"Jeff W Sanders and Paolo Zuliani . 2000 . Quantum programming . In International Conference on Mathematics of Program Construction. 80\u201399 . Jeff W Sanders and Paolo Zuliani. 2000. Quantum programming. In International Conference on Mathematics of Program Construction. 80\u201399."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703432165"},{"key":"e_1_3_2_1_27_1","volume-title":"Mathematical Foundations of Quantum Mechanics","author":"Neumann John Von","unstructured":"John Von Neumann . 1955. Mathematical Foundations of Quantum Mechanics . Princeton University Press , Princeton, NJ . John Von Neumann. 1955. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the ACM on Programming Languages, 7, POPL","author":"Zhou Li","year":"2023","unstructured":"Li Zhou , Gilles Barthe , Pierre-Yves Strub , Junyi Liu , and Mingsheng Ying . 2023 . CoqQ: Foundational Verification of Quantum Programs . Proceedings of the ACM on Programming Languages, 7, POPL (2023), 833\u2013865. Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs. Proceedings of the ACM on Programming Languages, 7, POPL (2023), 833\u2013865."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages. 179\u2013195","author":"Zuliani Paolo","year":"2004","unstructured":"Paolo Zuliani . 2004 . Non-deterministic quantum programming . In Proceedings of the 2nd International Workshop on Quantum Programming Languages. 179\u2013195 . Paolo Zuliani. 2004. Non-deterministic quantum programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages. 179\u2013195."}],"event":{"name":"ASPLOS '23: 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3","location":"Vancouver BC Canada","acronym":"ASPLOS '23","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3582016.3582039","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:45Z","timestamp":1750178805000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3582016.3582039"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,25]]},"references-count":30,"alternative-id":["10.1145\/3582016.3582039","10.1145\/3582016"],"URL":"https:\/\/doi.org\/10.1145\/3582016.3582039","relation":{},"subject":[],"published":{"date-parts":[[2023,3,25]]},"assertion":[{"value":"2023-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}