{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:07:15Z","timestamp":1753884435042,"version":"3.41.2"},"reference-count":58,"publisher":"World Scientific Pub Co Pte Ltd","issue":"06","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62072176"],"award-info":[{"award-number":["62072176"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61832015"],"award-info":[{"award-number":["61832015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2024,4]]},"abstract":"<jats:p> In order to verify the functional correctness of quantum circuits or algorithms, a prominent approach is to specify them as quantum programs and semi-automatically deduce them in a theorem prover. It is indispensable to first formalize the semantics of the basic quantum language. We formalize in Coq an imperative language which allows for classical and quantum information interactions. We define small-step operational semantics and state-based denotational semantics. Then we prove a consistency theorem between these two semantics. A distribution-based denotational semantics is also defined and related to the state-based one. Finally, we describe a few typical quantum algorithms and utilize the distribution-based denotational semantics to verify their correctness. <\/jats:p>","DOI":"10.1142\/s0218126624501123","type":"journal-article","created":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T10:17:14Z","timestamp":1695982634000},"source":"Crossref","is-referenced-by-count":1,"title":["Formalizing the Semantics of a Classical-Quantum Imperative Language in Coq"],"prefix":"10.1142","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3110-7825","authenticated-orcid":false,"given":"Wenjun","family":"Shi","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 3663 North Zhongshan Road, Shanghai 200062, P. R. China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5678-6538","authenticated-orcid":false,"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[{"name":"John Hopcroft Center of Computer Science, Shanghai Jiao Tong University, 800 Dongchuan Road, Shanghai 200240, P. R. China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0753-418X","authenticated-orcid":false,"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 3663 North Zhongshan Road, Shanghai 200062, P. R. China"}]}],"member":"219","published-online":{"date-parts":[[2023,10,27]]},"reference":[{"key":"S0218126624501123BIB001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01011339"},{"key":"S0218126624501123BIB002","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"S0218126624501123BIB004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"S0218126624501123BIB005","first-page":"414","volume-title":"Semantic Techniques in Quantum Computation","volume":"1","author":"Gay S. J.","year":"2010"},{"key":"S0218126624501123BIB006","doi-asserted-by":"publisher","DOI":"10.1109\/ICQNM.2007.21"},{"key":"S0218126624501123BIB007","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749908003530"},{"key":"S0218126624501123BIB009","first-page":"73","volume":"8","author":"Davidson T. A. S.","year":"2012","journal-title":"Int. J. Unconv. Comput."},{"key":"S0218126624501123BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_33"},{"key":"S0218126624501123BIB011","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_42"},{"key":"S0218126624501123BIB012","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646094"},{"key":"S0218126624501123BIB013","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00191-1"},{"key":"S0218126624501123BIB014","doi-asserted-by":"publisher","DOI":"10.1145\/2629680"},{"key":"S0218126624501123BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_33"},{"key":"S0218126624501123BIB016","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126623501669"},{"key":"S0218126624501123BIB017","first-page":"1","volume":"32","author":"haq Shaik E.","year":"2023","journal-title":"J. Circuits Syst. Comput."},{"key":"S0218126624501123BIB018","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126622502371"},{"key":"S0218126624501123BIB019","first-page":"197","volume":"2","author":"Gr\u00f6ssing G.","year":"1988","journal-title":"Complex Syst."},{"key":"S0218126624501123BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_7"},{"key":"S0218126624501123BIB021","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"S0218126624501123BIB022","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_24"},{"key":"S0218126624501123BIB023","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.09.001"},{"key":"S0218126624501123BIB024","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2018.01.005"},{"key":"S0218126624501123BIB025","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"S0218126624501123BIB026","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40313-2_35"},{"key":"S0218126624501123BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_17"},{"key":"S0218126624501123BIB028","first-page":"1","volume-title":"Proc. 28th Int. Conf. Concurrency Theory","author":"Feng Y.","year":"2017"},{"key":"S0218126624501123BIB030","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"S0218126624501123BIB031","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.02.017"},{"key":"S0218126624501123BIB032","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"S0218126624501123BIB033","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"S0218126624501123BIB034","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"S0218126624501123BIB035","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"S0218126624501123BIB036","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-021-1637-9"},{"key":"S0218126624501123BIB037","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"first-page":"119","volume-title":"Proc. 14th Int. Conf. Quantum Physics and Logic","author":"Rand R.","key":"S0218126624501123BIB038"},{"first-page":"299","volume-title":"Proc. 15th Int. Conf. Quantum Physics and Logic","author":"Rand R.","key":"S0218126624501123BIB039"},{"key":"S0218126624501123BIB040","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"first-page":"71","volume-title":"Proc. 12th Int. Workshop on Quantum Physics and Logic","author":"Boender J.","key":"S0218126624501123BIB041"},{"key":"S0218126624501123BIB042","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27818-4_7"},{"key":"S0218126624501123BIB043","volume":"12","author":"Cano G.","year":"2016","journal-title":"Log. Methods Comput. Sci."},{"key":"S0218126624501123BIB045","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09527-x"},{"key":"S0218126624501123BIB046","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S0218126624501123BIB047","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"S0218126624501123BIB048","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"S0218126624501123BIB050","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"S0218126624501123BIB051","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"volume-title":"Foundations of Quantum Programming","year":"2016","author":"Ying M.","key":"S0218126624501123BIB052"},{"volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","year":"2002","author":"Nipkow T.","key":"S0218126624501123BIB053"},{"key":"S0218126624501123BIB054","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854073"},{"key":"S0218126624501123BIB055","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9481-5"},{"key":"S0218126624501123BIB056","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"S0218126624501123BIB057","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"S0218126624501123BIB058","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"S0218126624501123BIB060","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00480-5"},{"key":"S0218126624501123BIB061","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_28"},{"key":"S0218126624501123BIB062","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"S0218126624501123BIB063","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"first-page":"1","volume-title":"Proc. 15th Int. Conf. Quantum Physics and Logic","author":"Amy M.","key":"S0218126624501123BIB064"}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126624501123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T08:32:26Z","timestamp":1712046746000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218126624501123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,27]]},"references-count":58,"journal-issue":{"issue":"06","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["10.1142\/S0218126624501123"],"URL":"https:\/\/doi.org\/10.1142\/s0218126624501123","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"type":"print","value":"0218-1266"},{"type":"electronic","value":"1793-6454"}],"subject":[],"published":{"date-parts":[[2023,10,27]]},"article-number":"2450112"}}