{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:47Z","timestamp":1780994627675,"version":"3.54.1"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.<\/jats:p>","DOI":"10.1145\/3571222","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"833-865","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["CoqQ: Foundational Verification of Quantum Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"first","affiliation":[{"name":"MPI-SP, Germany \/ Institute of Software at Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany \/ IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8196-7875","authenticated-orcid":false,"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"Meta, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5715-4885","authenticated-orcid":false,"given":"Junyi","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Categorical quantum mechanics. Handbook of quantum logic and quantum structures, 2","author":"Abramsky Samson","year":"2009","unstructured":"Samson Abramsky and Bob Coecke . 2009. Categorical quantum mechanics. Handbook of quantum logic and quantum structures, 2 ( 2009 ), 261\u2013325. Samson Abramsky and Bob Coecke. 2009. Categorical quantum mechanics. Handbook of quantum logic and quantum structures, 2 (2009), 261\u2013325."},{"key":"e_1_2_1_2_1","volume-title":"The Logic of Quantum Program Verification. Master\u2019s thesis","author":"Akatov Dmitri","unstructured":"Dmitri Akatov . 2005. The Logic of Quantum Program Verification. Master\u2019s thesis . Oxford University Computing Laboratory . Dmitri Akatov. 2005. The Logic of Quantum Program Verification. Master\u2019s thesis. Oxford University Computing Laboratory."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2562110"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_2_1_5_1","volume-title":"European Symposium on Programming. 1\u201317","author":"Appel Andrew W","year":"2011","unstructured":"Andrew W Appel . 2011 . Verified software toolchain . In European Symposium on Programming. 1\u201317 . Andrew W Appel. 2011. Verified software toolchain. In European Symposium on Programming. 1\u201317."},{"key":"e_1_2_1_6_1","volume-title":"LQP: the dynamic logic of quantum information. Mathematical structures in computer science, 16, 3","author":"Baltag Alexandru","year":"2006","unstructured":"Alexandru Baltag and Sonja Smets . 2006. LQP: the dynamic logic of quantum information. Mathematical structures in computer science, 16, 3 ( 2006 ), 491\u2013525. Alexandru Baltag and Sonja Smets. 2006. LQP: the dynamic logic of quantum information. Mathematical structures in computer science, 16, 3 (2006), 491\u2013525."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484567"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9481-5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aar3106"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_1_14_1","volume-title":"Complex Bounded Operators. Archive of Formal Proofs (Sept","author":"Rodriguez Caballero Jose Manuel","year":"2021","unstructured":"Jose Manuel Rodriguez Caballero and Dominique Unruh . 2021. Complex Bounded Operators. Archive of Formal Proofs (Sept . 2021 )., https:\/\/isa-afp.org\/entries\/Complex_Bounded_Operators.html Jose Manuel Rodriguez Caballero and Dominique Unruh. 2021. Complex Bounded Operators. Archive of Formal Proofs (Sept. 2021)., https:\/\/isa-afp.org\/entries\/Complex_Bounded_Operators.html"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_1_16_1","volume-title":"AIP Conference Proceedings. 810","author":"Coecke Bob","year":"2006","unstructured":"Bob Coecke . 2006 . Kindergarten quantum mechanics: Lecture notes . In AIP Conference Proceedings. 810 , 81\u201398. Bob Coecke. 2006. Kindergarten quantum mechanics: Lecture notes. In AIP Conference Proceedings. 810, 81\u201398."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2020-06-04-279"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000051"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation. 333\u2013342","author":"Green Alexander S","year":"2013","unstructured":"Alexander S Green , Peter LeFanu Lumsdaine , Neil J Ross , Peter Selinger , and Beno\u00eet Valiron . 2013 . Quipper: a scalable quantum programming language . In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation. 333\u2013342 . Alexander S Green, Peter LeFanu Lumsdaine, Neil J Ross, Peter Selinger, and Beno\u00eet Valiron. 2013. Quipper: a scalable quantum programming language. In Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation. 333\u2013342."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209128"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209139"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_33_1","volume-title":"Annual Asian Computing Science Conference. 79\u201393","author":"Kakutani Yoshihiko","year":"2009","unstructured":"Yoshihiko Kakutani . 2009 . A logic for formal verification of quantum programs . In Annual Asian Computing Science Conference. 79\u201393 . Yoshihiko Kakutani. 2009. A logic for formal verification of quantum programs. In Annual Asian Computing Science Conference. 79\u201393."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.318.14"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_22"},{"key":"e_1_2_1_36_1","volume-title":"TR96-003","author":"Kitaev Alexei Y.","year":"1996","unstructured":"Alexei Y. Kitaev . 1996. Quantum measurements and the Abelian Stabilizer Problem. Electron. Colloquium Comput. Complex ., TR96-003 ( 1996 ), ECCC :. arxiv:quant-ph\/9511026 Alexei Y. Kitaev. 1996. Quantum measurements and the Abelian Stabilizer Problem. Electron. Colloquium Comput. Complex., TR96-003 (1996), ECCC:. arxiv:quant-ph\/9511026"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings 19th International Conference on Quantum Physics and Logic, QPL 2022","author":"Lehmann Adrian","year":"2022","unstructured":"Adrian Lehmann , Ben Caldwell , and Robert Rand . 2022 . VyZX : A Vision for Verifying the ZX Calculus . In Proceedings 19th International Conference on Quantum Physics and Logic, QPL 2022 , Oxford, England, 27 June \u2013 1 July 2012, to be published, Bob Coecke and Matthew Leifer (Eds.). arxiv:arXiv preprint arXiv:1908.08963. arxiv:2205.05781 Adrian Lehmann, Ben Caldwell, and Robert Rand. 2022. VyZX : A Vision for Verifying the ZX Calculus. In Proceedings 19th International Conference on Quantum Physics and Logic, QPL 2022, Oxford, England, 27 June \u2013 1 July 2012, to be published, Bob Coecke and Matthew Leifer (Eds.). arxiv:arXiv preprint arXiv:1908.08963. arxiv:2205.05781"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_2_1_41_1","volume-title":"International conference on computer aided verification. 187\u2013207","author":"Liu Junyi","year":"2019","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 . In International conference on computer aided verification. 187\u2013207 . 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. In International conference on computer aided verification. 187\u2013207."},{"key":"#cr-split#-e_1_2_1_42_1.1","unstructured":"Chris Lomont. 2004. The Hidden Subgroup Problem - Review and Open Problems. https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0411037 10.48550\/arxiv.quant-ph"},{"key":"#cr-split#-e_1_2_1_42_1.2","unstructured":"Chris Lomont. 2004. The Hidden Subgroup Problem - Review and Open Problems. https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0411037"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Michael A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information. \t\t\t\t  Michael A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information.","DOI":"10.1119\/1.1463744"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/JETCAS.2022.3202204"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523713"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_2_1_50_1","volume-title":"The Fourth International Workshop on Coq for Programming Languages.","author":"Rand Robert","year":"2018","unstructured":"Robert Rand , Jennifer Paykin , and Steve Zdancewic . 2018 . Phantom types for quantum programs . In The Fourth International Workshop on Coq for Programming Languages. Robert Rand, Jennifer Paykin, and Steve Zdancewic. 2018. Phantom types for quantum programs. In The Fourth International Workshop on Coq for Programming Languages."},{"key":"e_1_2_1_51_1","volume-title":"Linear representations of finite groups. 42","author":"Serre Jean-Pierre","unstructured":"Jean-Pierre Serre . 1977. Linear representations of finite groups. 42 , Springer . Jean-Pierre Serre. 1977. Linear representations of finite groups. 42, Springer."},{"key":"e_1_2_1_52_1","volume-title":"Quantum Hoare Type Theory. Master\u2019s thesis","author":"Singhal Kartik","year":"2012","unstructured":"Kartik Singhal . 2020. Quantum Hoare Type Theory. Master\u2019s thesis . University of Chicago . Chicago, IL. arxiv: 2012 .02154. https:\/\/ks.cs.uchicago.edu\/publication\/qhtt-masters\/ See also: https:\/\/ks.cs.uchicago.edu\/publication\/qhtt\/ Kartik Singhal. 2020. Quantum Hoare Type Theory. Master\u2019s thesis. University of Chicago. Chicago, IL. arxiv:2012.02154. https:\/\/ks.cs.uchicago.edu\/publication\/qhtt-masters\/ See also: https:\/\/ks.cs.uchicago.edu\/publication\/qhtt\/"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_1_54_1","unstructured":"The Cirq Developers. 2018. quantumlib\/Cirq: A Python framework for creating editing and invoking Noisy Intermediate Scale Quantum (NISQ) circuits. https:\/\/github.com\/quantumlib\/Cirq \t\t\t\t  The Cirq Developers. 2018. quantumlib\/Cirq: A Python framework for creating editing and invoking Noisy Intermediate Scale Quantum (NISQ) circuits. https:\/\/github.com\/quantumlib\/Cirq"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_2_1_56_1","volume-title":"MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis Since","author":"MathComp Analysis Development The","year":"2017","unstructured":"The MathComp Analysis Development Team. 2022. MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis Since 2017 . Version 0.5.1 The MathComp Analysis Development Team. 2022. MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis Since 2017. Version 0.5.1"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854073"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_1_60_1","volume-title":"Advances in Cryptology \u2013 ASIACRYPT","author":"Unruh Dominique","year":"2020","unstructured":"Dominique Unruh . 2020. Post-Quantum Verification of Fujisaki-Okamoto . In Advances in Cryptology \u2013 ASIACRYPT 2020 , Shiho Moriai and Huaxiong Wang (Eds.). Springer International Publishing , Cham. 321\u2013352. isbn:978-3-030-64837-4 Dominique Unruh. 2020. Post-Quantum Verification of Fujisaki-Okamoto. In Advances in Cryptology \u2013 ASIACRYPT 2020, Shiho Moriai and Huaxiong Wang (Eds.). Springer International Publishing, Cham. 321\u2013352. isbn:978-3-030-64837-4"},{"key":"e_1_2_1_61_1","volume-title":"The Second International Workshop on Programming Languages for Quantum Computing (PLanQC","author":"Unruh Dominique","year":"2021","unstructured":"Dominique Unruh . 2021 . Quantum and classical registers . In The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021). arxiv:2105.10914 Dominique Unruh. 2021. Quantum and classical registers. In The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021). arxiv:2105.10914"},{"key":"e_1_2_1_62_1","volume-title":"2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201310","author":"Vilmart Renaud","year":"2019","unstructured":"Renaud Vilmart . 2019 . A near-minimal axiomatisation of zx-calculus for pure qubit quantum mechanics . In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201310 . Renaud Vilmart. 2019. A near-minimal axiomatisation of zx-calculus for pure qubit quantum mechanics. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201310."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan-Kaufmann. \t\t\t\t  Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan-Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00005-7"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0465-3"},{"key":"#cr-split#-e_1_2_1_66_1.1","unstructured":"Mingsheng Ying Li Zhou and Yangjia Li. 2018. Reasoning about Parallel Quantum Programs. https:\/\/doi.org\/10.48550\/arxiv.1810.11334 10.48550\/arxiv.1810.11334"},{"key":"#cr-split#-e_1_2_1_66_1.2","unstructured":"Mingsheng Ying Li Zhou and Yangjia Li. 2018. Reasoning about Parallel Quantum Programs. https:\/\/doi.org\/10.48550\/arxiv.1810.11334"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.10.025"},{"key":"#cr-split#-e_1_2_1_68_1.1","unstructured":"Nengkun Yu. 2019. Quantum Temporal Logic. https:\/\/doi.org\/10.48550\/arxiv.1908.00158 10.48550\/arxiv.1908.00158"},{"key":"#cr-split#-e_1_2_1_68_1.2","unstructured":"Nengkun Yu. 2019. Quantum Temporal Logic. https:\/\/doi.org\/10.48550\/arxiv.1908.00158"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563297"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498691"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554343"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571222","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571222","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571222"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":77,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571222"],"URL":"https:\/\/doi.org\/10.1145\/3571222","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}