{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T12:51:05Z","timestamp":1775739065059,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100012537","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DE180100156, DP180100691"],"award-info":[{"award-number":["DE180100156, DP180100691"]}],"id":[{"id":"10.13039\/100012537","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61832015"],"award-info":[{"award-number":["61832015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Key R&D Program of China","award":["2018YFA0306701"],"award-info":[{"award-number":["2018YFA0306701"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314584","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1149-1162","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["An applied quantum Hoare logic"],"prefix":"10.1145","author":[{"given":"Li","family":"Zhou","sequence":"first","affiliation":[{"name":"Tsinghua University, China"}]},{"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_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. Dept. of Computer Science, Princeton University NJ. ftp:\/\/ftp.cs.princeton.edu\/reports\/2012\/934.pdf. 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. Dept. of Computer Science, Princeton University NJ. ftp:\/\/ftp.cs.princeton.edu\/reports\/2012\/934.pdf."},{"key":"e_1_3_2_2_2_1","volume-title":"The Logic of Quantum Program Verification. Master's thesis","author":"Akatov Dmitri","unstructured":"Dmitri Akatov . 2005. The Logic of Quantum Program Verification. Master's thesis . Oxford University Computing Laboratory . http:\/\/www.academia.edu\/download\/7563948\/thesis-1.1.ps. Dmitri Akatov. 2005. The Logic of Quantum Program Verification. Master's thesis. Oxford University Computing Laboratory. http:\/\/www.academia.edu\/download\/7563948\/thesis-1.1.ps."},{"key":"e_1_3_2_2_3_1","unstructured":"Gadi Aleksandrowicz Thomas Alexander Panagiotis Barkoutsos Luciano Bello Yael Ben-Haim David Bucher Francisco Jose Cabrera-Hern\u00e1dez Jorge Carballo-Franquis Adrian Chen Chun-Fu Chen Jerry M. Chow Antonio D. C\u00f3rcoles-Gonzales Abigail J. Cross Andrew Cross Juan Cruz-Benito Chris Culver Salvador De La Puente Gonz\u00e1lez Enrique De La Torre Delton Ding Eugene Dumitrescu Ivan Duran Pieter Eendebak Mark Everitt Ismael Faro Sertage Albert Frisch Andreas Fuhrer Jay Gambetta Borja Godoy Gago Juan Gomez-Mosquera Donny Greenberg Ikko Hamamura Vojtech Havlicek Joe Hellmers ?ukasz Herok Hiroshi Horii Shaohan Hu Takashi Imamichi Toshinari Itoko Ali Javadi-Abhari Naoki Kanazawa Anton Karazeev Kevin Krsulich Peng Liu Yang Luh Yunho Maeng Manoel Marques Francisco Jose Mart\u00edn-Fern\u00e1ndez Douglas T. McClure David McKay Srujan Meesala Antonio Mezzacapo Nikolaj Moll Diego Moreda Rodr\u00edguez Giacomo Nannicini Paul Nation Pauline Ollitrault Lee James O'Riordan Hanhee Paik Jes\u00fas P\u00e9rez Anna Phan Marco Pistoia Viktor Prutyanov Max Reuter Julia Rice Abd\u00f3n Rodr\u00edguez Davila Raymond Harry Putra Rudy Mingi Ryu Ninad Sathaye Chris Schnabel Eddie Schoute Kanav Setia Yunong Shi Adenilton Silva Yukio Siraichi Seyon Sivarajah John A. Smolin Mathias Soeken Hitomi Takahashi Ivano Tavernelli Charles Taylor Pete Taylour Kenso Trabing Matthew Treinish Wes Turner Desiree Vogt-Lee Christophe Vuillot Jonathan A. Wildstrom Jessica Wilson Erick Winston Christopher Wood Stephen Wood Stefan W\u00f6rner Ismail Yunus Akhalwaya and Christa Zoufal. 2019. Qiskit: An Open-source Framework for Quantum Computing.  Gadi Aleksandrowicz Thomas Alexander Panagiotis Barkoutsos Luciano Bello Yael Ben-Haim David Bucher Francisco Jose Cabrera-Hern\u00e1dez Jorge Carballo-Franquis Adrian Chen Chun-Fu Chen Jerry M. Chow Antonio D. C\u00f3rcoles-Gonzales Abigail J. Cross Andrew Cross Juan Cruz-Benito Chris Culver Salvador De La Puente Gonz\u00e1lez Enrique De La Torre Delton Ding Eugene Dumitrescu Ivan Duran Pieter Eendebak Mark Everitt Ismael Faro Sertage Albert Frisch Andreas Fuhrer Jay Gambetta Borja Godoy Gago Juan Gomez-Mosquera Donny Greenberg Ikko Hamamura Vojtech Havlicek Joe Hellmers ?ukasz Herok Hiroshi Horii Shaohan Hu Takashi Imamichi Toshinari Itoko Ali Javadi-Abhari Naoki Kanazawa Anton Karazeev Kevin Krsulich Peng Liu Yang Luh Yunho Maeng Manoel Marques Francisco Jose Mart\u00edn-Fern\u00e1ndez Douglas T. McClure David McKay Srujan Meesala Antonio Mezzacapo Nikolaj Moll Diego Moreda Rodr\u00edguez Giacomo Nannicini Paul Nation Pauline Ollitrault Lee James O'Riordan Hanhee Paik Jes\u00fas P\u00e9rez Anna Phan Marco Pistoia Viktor Prutyanov Max Reuter Julia Rice Abd\u00f3n Rodr\u00edguez Davila Raymond Harry Putra Rudy Mingi Ryu Ninad Sathaye Chris Schnabel Eddie Schoute Kanav Setia Yunong Shi Adenilton Silva Yukio Siraichi Seyon Sivarajah John A. Smolin Mathias Soeken Hitomi Takahashi Ivano Tavernelli Charles Taylor Pete Taylour Kenso Trabing Matthew Treinish Wes Turner Desiree Vogt-Lee Christophe Vuillot Jonathan A. Wildstrom Jessica Wilson Erick Winston Christopher Wood Stephen Wood Stefan W\u00f6rner Ismail Yunus Akhalwaya and Christa Zoufal. 2019. Qiskit: An Open-source Framework for Quantum Computing."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1137\/130939043"},{"key":"e_1_3_2_2_6_1","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL 2004","author":"Baltag Alexandru","year":"2004","unstructured":"Alexandru Baltag and Sonja Smets . 2004 . The logic of quantum programs . In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL 2004 ), Peter Selinger (Ed.). 39-56. https:\/\/www.mathstat.dal.ca\/~selinger\/qpl 2004\/PDFS\/04Baltag-Smets.pdf. Alexandru Baltag and Sonja Smets. 2004. The logic of quantum programs. In Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL 2004), Peter Selinger (Ed.). 39-56. https:\/\/www.mathstat.dal.ca\/~selinger\/qpl2004\/PDFS\/04Baltag-Smets.pdf."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_3_2_2_16_1","unstructured":"Google AI Quantum team. 2018. https:\/\/github.com\/quantumlib\/Cirq.  Google AI Quantum team. 2018. https:\/\/github.com\/quantumlib\/Cirq."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1562764.1562779"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_2_22_1","volume-title":"Orthomodular lattices","author":"Kalmbach Gudrun","unstructured":"Gudrun Kalmbach . 1983. Orthomodular lattices . Vol. 18 . Academic Press .. Gudrun Kalmbach. 1983. Orthomodular lattices. Vol. 18. Academic Press.."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158123"},{"key":"e_1_3_2_2_24_1","volume-title":"A theorem prover for quantum Hoare logic and its applications. arXiv preprint arXiv:1601.03835","author":"Liu Tao","year":"2016","unstructured":"Tao Liu , Yangjia Li , Shuling Wang , Mingsheng Ying , and Naijun Zhan . 2016. A theorem prover for quantum Hoare logic and its applications. arXiv preprint arXiv:1601.03835 ( 2016 ). https:\/\/arxiv.org\/abs\/1601.03835. Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, and Naijun Zhan. 2016. A theorem prover for quantum Hoare logic and its applications. arXiv preprint arXiv:1601.03835 (2016). https:\/\/arxiv.org\/abs\/1601.03835."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1038\/nphys3029"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00453-013-9826-8"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_2_29_1","unstructured":"Robert Rand. 2016. Verification logics for quantum programs. http:\/\/www.cs.umd.edu\/~rrand\/wpe.pdf.  Robert Rand. 2016. Verification logics for quantum programs. http:\/\/www.cs.umd.edu\/~rrand\/wpe.pdf."},{"key":"e_1_3_2_2_30_1","unstructured":"Rigetti Forest team. 2018. https:\/\/www.rigetti.com\/forest.  Rigetti Forest team. 2018. https:\/\/www.rigetti.com\/forest."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/648085.747181"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.796385"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_2_38_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.00005-7"},{"key":"e_1_3_2_2_39_1","first-page":"311","article-title":"Predicate transformer semantics of quantum programs","volume":"8","author":"Ying Mingsheng","year":"2010","unstructured":"Mingsheng Ying , Runyao Duan , Yuan Feng , and Zhengfeng Ji . 2010 . Predicate transformer semantics of quantum programs . Semantic Techniques in Quantum Computation 8 (2010), 311 - 360 .. Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. 2010. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation 8 (2010), 311-360..","journal-title":"Semantic Techniques in Quantum Computation"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009840"},{"key":"e_1_3_2_2_41_1","unstructured":"Li Zhou Nengkun Yu and Mingsheng Ying. In preparation. Testing and debugging of quantum programs. (In preparation)..  Li Zhou Nengkun Yu and Mingsheng Ying. In preparation. Testing and debugging of quantum programs. (In preparation).."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314584","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314584","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314584"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":40,"alternative-id":["10.1145\/3314221.3314584","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314584","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}