{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:33Z","timestamp":1780994613833,"version":"3.54.1"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key R&D Program of China","doi-asserted-by":"crossref","award":["2023YFA1009403"],"award-info":[{"award-number":["2023YFA1009403"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["EXC 2092 CASA - 390781972"],"award-info":[{"award-number":["EXC 2092 CASA - 390781972"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Dirac notation is widely used in quantum physics and quantum programming languages to define, compute and reason about quantum states. This paper considers Dirac notation from the perspective of automated reasoning. We prove two main results: first, the first-order theory of Dirac notation is decidable, by a reduction to the theory of real closed fields and Tarski\u2019s theorem. Then, we prove that validity of equations can be decided efficiently, using term-rewriting techniques. We implement our equivalence checking algorithm in Mathematica, and showcase its efficiency across more than 100 examples from the literature.<\/jats:p>","DOI":"10.1145\/3704878","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1227-1259","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Automating Equational Proofs in Dirac Notation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9071-7862","authenticated-orcid":false,"given":"Yingte","family":"Xu","sequence":"first","affiliation":[{"name":"MPI-SP, Bochum, Germany"},{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, 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, Bochum, Germany"},{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319636"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.287.1"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.384.8"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:8)2017"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Thomas Arts and J\u00fcrgen Giesl. 2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science 236 (4 2000) 133\u2013178. Issue 1-2. https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8 10.1016\/S0304-3975(99)00207-8","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Miriam Backens and Aleks Kissinger. 2018. ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity. In Proceedings 15th International Conference on Quantum Physics and Logic QPL 2018 Halifax Canada 3-7th 7une 2018 (EPTCS Vol. 287) Peter Selinger and Giulio Chiribella (Eds.). 23\u201342. https:\/\/doi.org\/10.4204\/EPTCS.287.2 10.4204\/EPTCS.287.2","DOI":"10.4204\/EPTCS.287.2"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80027-5"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Yves Bertot Georges Gonthier Sidi Ould Biha and Ioana Pasca. 2008. Canonical Big Operators. (2008) 86\u2013101. https:\/\/doi.org\/10.1007\/978-3-540-71067-7_11 10.1007\/978-3-540-71067-7_11","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000120"},{"key":"e_1_3_2_13_2","article-title":"Isabelle marries dirac: A library for quantum computation and quantum information","author":"Bordg Anthony","year":"2020","unstructured":"Anthony Bordg, Hanna Lachnitt, and Yijun He. 2020. Isabelle marries dirac: A library for quantum computation and quantum information. Archive of Formal Proofs (2020).","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Titouan Carette Timoth\u00e9e Hoffreumon \u00c9mile Larroque and Renaud Vilmart. 2023. Complete Graphical Language for Hermiticity-Preserving Superoperators. In 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201322. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175712 10.1109\/LICS56636.2023.10175712","DOI":"10.1109\/LICS56636.2023.10175712"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1201\/9781003090052-7"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1093390.1093393"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"\u00c9velyne Contejean Pierre Courtieu Julien Forest Olivier Pons and Xavier Urbain. 2011. Automated Certified Proofs with CiME3. 10 (2011) 21\u201330. https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.21 10.4230\/LIPIcs.RTA.2011.21","DOI":"10.4230\/LIPIcs.RTA.2011.21"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_13"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71069-3_22"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100021162"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2020-06-04-279"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Alejandro D\u00edaz-Caro Gilles Dowek and Juan Pablo Rinaldi. 2019. Two linearities for quantum computing in the lambda calculus. Biosystems 186 (2019) 104012. https:\/\/doi.org\/10.1016\/j.biosystems.2019.104012 10.1016\/j.biosystems.2019.104012 Selected papers from the International Conference on the Theory and Practice of Natural Computing 2017.","DOI":"10.1016\/j.biosystems.2019.104012"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Alejandro D\u00edaz-Caro Mauricio Guillermo Alexandre Miquel and Beno\u00eet Valiron. 2019. Realizability in the Unitary Sphere. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. https:\/\/doi.org\/10.1109\/LICS.2019.8785834 10.1109\/LICS.2019.8785834","DOI":"10.1109\/LICS.2019.8785834"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-023-09689-9"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Yuan Feng and Sanjiang Li. 2023. Abstract interpretation Hoare logic and incorrectness logic for quantum programs. Information and Computation 294 (2023) 105077. https:\/\/doi.org\/10.1016\/j.ic.2023.105077 10.1016\/j.ic.2023.105077","DOI":"10.1016\/j.ic.2023.105077"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_3_2_32_2","volume-title":"Stability, Simplicity and the Model Theory of Bilinear Forms","author":"Granger Nicolas","year":"1999","unstructured":"Nicolas Granger. 1999. Stability, Simplicity and the Model Theory of Bilinear Forms. Ph. D. Dissertation. University of Manchester."},{"key":"e_1_3_2_33_2","unstructured":"Alexander S Green Peter LeFanu Lumsdaine Neil J Ross DalCa Peter Selinger and Beno^1tBeno^1t Valiron. [n. d.]. Quipper: a scalable quantum programming language. dl.acm.org ([n. d.]). https:\/\/dl.acm.org\/doi\/abs\/10.1145\/2491956.2462177"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78127-1_20"},{"key":"e_1_3_2_36_2","unstructured":"Kesha Hietala Sarah Marshall Robert Rand and Nikhil Swamy. [n. d.]. Q*: Implementing Quantum Separation Logic in F. ([n. d.])."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Kesha Hietala Robert Rand Shih-Han Hung Xiaodi Wu and Michael Hicks. 2021. A verified optimizer for Quantum circuits. 5 POPL Article 37 (jan 2021) 29 pages. https:\/\/doi.org\/10.1145\/3434318 10.1145\/3434318","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_40_2","unstructured":"Xin Hong Wei-Jia Huang Wei-Chen Chien Yuan Feng Min-Hsiu Hsieh Sanjiang Li and Mingsheng Ying. 2024. Equivalence Checking of Parameterised Quantum Circuits. (2024). arXiv:2404.18456 [quant-ph] https:\/\/arxiv.org\/abs\/2404.18456"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Shih-Han Hung Kesha Hietala Shaopeng Zhu Mingsheng Ying Michael Hicks and Xiaodi Wu. 2019. Quantitative robustness analysis of quantum programs. 3 POPL Article 31 (jan 2019) 29 pages. https:\/\/doi.org\/10.1145\/3290344 10.1145\/3290344","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209131"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.318.14"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2011.01.035"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950800741X"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_2_47_2","unstructured":"Adrian Lehmann Ben Caldwell and Robert Rand. 2022. VyZX: A Vision for Verifying the ZX Calculus. (2022). arXiv:2205.05781 [quant-ph] https:\/\/arxiv.org\/abs\/2205.05781"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Marco Lewis Sadegh Soudjani and Paolo Zuliani. 2023. Formal Verification of Quantum Programs: Theory Tools and Challenges. 5 1 Article 1 (dec 2023) 35 pages. https:\/\/doi.org\/10.1145\/3624483 10.1145\/3624483","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_50_2","unstructured":"Liyi Li Mingwei Zhu Rance Cleaveland Alexander Nicolellis Yi Lee Le Chang and Xiaodi Wu. 2024. Qafny: A Quantum-Program Verifier. (2024). arXiv:2211.06411 [quant-ph] https:\/\/arxiv.org\/abs\/2211.06411"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_2_52_2","first-page":"441","volume-title":"Kreiseliana: About and Around Georg Kreisel","author":"Macintyre Angus","year":"1996","unstructured":"Angus Macintyre and Alex J. Wilkie. 1996. On the Decidability of the Real Exponential Field. In Kreiseliana: About and Around Georg Kreisel, Piergiorgio Odifreddi (Ed.). A K Peters, 441\u2013467."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"Jens Palsberg and Nengkun Yu. 2024. Optimal implementation of quantum gates with two controls. Linear Algebra Appl. 694 (2024) 206\u2013261. https:\/\/doi.org\/10.1016\/j.laa.2024.03.039 10.1016\/j.laa.2024.03.039","DOI":"10.1016\/j.laa.2024.03.039"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009894"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Boldizs\u00e1r Po\u00f3r Quanlong Wang Razin A. Shaikh Lia Yeh Richie Yeung and Bob Coecke. 2023. Completeness for arbitrary finite dimensions of ZXW-calculus a unifying calculus. In 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201314. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175672 10.1109\/LICS56636.2023.10175672","DOI":"10.1109\/LICS56636.2023.10175672"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Robert Rand Jennifer Paykin and Steve Zdancewic. 2017. QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In Proceedings 14th International Conference on Quantum Physics and Logic QPL 2017 Nijmegen The Netherlands 3-7 7uly 2017. (EPTCS Vol. 266) Bob Coecke and Aleks Kissinger (Eds.). 119\u2013132. https:\/\/doi.org\/10.4204\/EPTCS.266.8 10.4204\/EPTCS.266.8","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"Rodrigo Raya and Viktor Kuncak. 2024. On algebraic array theories. 7. Log. Algebraic Methods Program. 136 (2024) 100906. https:\/\/doi.org\/10.1016\/J.JLAMP.2023.100906 10.1016\/J.JLAMP.2023.100906","DOI":"10.1016\/J.JLAMP.2023.100906"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2011.01.010"},{"key":"e_1_3_2_62_2","unstructured":"Kartik Singhal ROBERT Rand and MATTHEW Amy. 2022. Beyond separation: Toward a specification language for modular reasoning about quantum programs. Programming Languages for Quantum Computing (PLanQC) 2022 Poster Abstract (2022)."},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.APAL.2012.04.003"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"e_1_3_2_66_2","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."},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"Dominique Unruh. 2019. Quantum Hoare Logic with Ghost Variables. In 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. https:\/\/doi.org\/10.1109\/LICS.2019.8785779 10.1109\/LICS.2019.8785779","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_69_2","unstructured":"John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] https:\/\/arxiv.org\/abs\/2012.13966"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2023.36"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","unstructured":"Yingte Xu Gilles Barthe and Li Zhou. 2024. Automating Equational Proofs in Dirac Notation. (2024). arXiv:2411.11617 [cs.PL] https:\/\/doi.org\/10.48550\/arXiv.2411.11617 10.48550\/arXiv.2411.11617","DOI":"10.48550\/arXiv.2411.11617"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","unstructured":"Yingte Xu zhou31416 and Pierre-Yves Strub. 2024. LucianoXu\/DiracImplementation: artifact-evaluation. https:\/\/doi.org\/10.5281\/zenodo.13924906 10.5281\/zenodo.13924906","DOI":"10.5281\/zenodo.13924906"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_74_2","volume-title":"Foundations of quantum programming","author":"Ying Mingsheng","year":"2016","unstructured":"Mingsheng Ying. 2016. Foundations of quantum programming. Morgan Kaufmann."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","unstructured":"Li Zhou Gilles Barthe Justin Hsu Mingsheng Ying and Nengkun Yu. 2021. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. In 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1-14. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470673 10.1109\/LICS52264.2021.9470673","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_3_2_78_2","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\/3704878","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:42Z","timestamp":1770200322000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":77,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704878"],"URL":"https:\/\/doi.org\/10.1145\/3704878","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}