{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:04Z","timestamp":1781238904789,"version":"3.54.1"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2011,12,1]],"date-time":"2011-12-01T00:00:00Z","timestamp":1322697600000},"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":["DP110103473"],"award-info":[{"award-number":["DP110103473"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["60736011"],"award-info":[{"award-number":["60736011"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,12]]},"abstract":"<jats:p>Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd--Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.<\/jats:p>","DOI":"10.1145\/2049706.2049708","type":"journal-article","created":{"date-parts":[[2011,12,30]],"date-time":"2011-12-30T17:01:45Z","timestamp":1325264505000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":129,"title":["Floyd--hoare logic for quantum programs"],"prefix":"10.1145","volume":"33","author":[{"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"University of Technology, Sydney and Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,1,3]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Akatov D. 2005. The logic of quantum program verification. M.S. thesis Oxford University Computing Laboratory.  Akatov D. 2005. The logic of quantum program verification. M.S. thesis Oxford University Computing Laboratory."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Apt K. R. and Olderog E. R. 1997. Verification of Sequential and Concurrent Programs. Springer Berlin.   Apt K. R. and Olderog E. R. 1997. Verification of Sequential and Concurrent Programs. Springer Berlin.","DOI":"10.1007\/978-1-4757-2714-2"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04)","author":"Baltag A."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_2_1_6_1","first-page":"181","article-title":"Toward an architecture for quantum programming. Euro","volume":"25","author":"Bettelli S.","year":"2003","journal-title":"Phys. J. D"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926446"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040318"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/977091.977108"},{"key":"e_1_2_1_17_1","volume-title":"Conventions for quantum pseudocode. Tech. rep. LAUR-96-2724","author":"Knill E. H.","year":"1996"},{"key":"e_1_2_1_18_1","unstructured":"Morgan C. 1995. Proof rules for probabilistic loops. Tech. rep. PRG-TR-25-95 Programming Research Group Oxford University.  Morgan C. 1995. Proof rules for probabilistic loops. Tech. rep. PRG-TR-25-95 Programming Research Group Oxford University."},{"key":"e_1_2_1_19_1","unstructured":"Nielsen I. L. and Chuang M. A. 2000. Quantum Computation and Quantum Information. Cambridge University Press Cambridge UK.   Nielsen I. L. and Chuang M. A. 2000. Quantum Computation and Quantum Information. Cambridge University Press Cambridge UK."},{"key":"e_1_2_1_20_1","unstructured":"\u00d6mer B. 2003. Structural quantum programming. Ph.D. dissertation Technical University of Vienna.  \u00d6mer B. 2003. Structural quantum programming. Ph.D. dissertation Technical University of Vienna."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Sanders J. W.\n     and \n      \n      \n      Zuliani P\n      \n  \n  . \n  2000\n  . Quantum programming. In Mathematics of Program Construction Lecture Notes in Computer Science vol. \n  1837\n  . \n  Springer Berlin 88--99.   Sanders J. W. and Zuliani P. 2000. Quantum programming. In Mathematics of Program Construction Lecture Notes in Computer Science vol. 1837. Springer Berlin 88--99.","DOI":"10.1007\/10722010_6"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 7th International Symposium on Functional and Logic Programming","author":"Selinger P."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_24_1","first-page":"1","article-title":"On infinite direct products","volume":"6","author":"Von Neumann J.","year":"1938","journal-title":"Compos. Math."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Ying M. S. Duan R. Y. Feng Y. and Ji Z. F. 2010. Predicate Transformer Semantics of Quantum Programs. Cambridge University Press 311--360.  Ying M. S. Duan R. Y. Feng Y. and Ji Z. F. 2010. Predicate Transformer Semantics of Quantum Programs. Cambridge University Press 311--360.","DOI":"10.1017\/CBO9781139193313.009"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507249"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages (QPL'04)","author":"Zuliani P.","year":"2004"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2049706.2049708","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2049706.2049708","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:41Z","timestamp":1750278401000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2049706.2049708"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["10.1145\/2049706.2049708"],"URL":"https:\/\/doi.org\/10.1145\/2049706.2049708","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12]]},"assertion":[{"value":"2010-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}