{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:25:44Z","timestamp":1760142344501,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is supported by a rich equational theory for proving equality between expressions in the language. These proofs are typically carried on pen-and-paper, and can be exceedingly long and error-prone. We introduce D-Hammer, the first tool to support automated equational proof for labelled Dirac notation. The salient features of D-Hammer include: an expressive, higher-order, dependently-typed language for labelled Dirac notation; an efficient normalization algorithm; and an optimized <jats:bold>++<\/jats:bold> implementation. We evaluate the implementation on representative examples from both plain and labelled Dirac notation. In the case of plain Dirac notation, we show that our implementation significantly outperforms DiracDec (Xu et al., POPL\u201925).<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_3","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:09Z","timestamp":1753155129000},"page":"53-76","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["D-Hammer: Efficient Equational Reasoning for\u00a0Labelled Dirac Notation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9071-7862","authenticated-orcid":false,"given":"Yingte","family":"Xu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9868-8477","authenticated-orcid":false,"given":"Li","family":"Zhou","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et al.: Verifying quantum circuits with level-synchronized tree automata. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704868","key":"3_CR1","DOI":"10.1145\/3704868"},{"doi-asserted-by":"publisher","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14\u201317 July 2004, Turku, Finland, Proceedings, pp. 415\u2013425. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319636","key":"3_CR2","DOI":"10.1109\/LICS.2004.1319636"},{"doi-asserted-by":"publisher","unstructured":"Acuaviva, A., et al.: The minimal canonical form of a tensor network. In: 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS), pp. 328\u2013362. IEEE, November 2023. https:\/\/doi.org\/10.1109\/focs57990.2023.00027, http:\/\/dx.doi.org\/10.1109\/FOCS57990.2023.00027","key":"3_CR3","DOI":"10.1109\/focs57990.2023.00027"},{"doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electron. Proc. Theor. Comput. Sci. 287, 1\u201321 (2019)","key":"3_CR4","DOI":"10.4204\/EPTCS.287.1"},{"issue":"9","key":"3_CR5","doi-asserted-by":"publisher","first-page":"093021","DOI":"10.1088\/1367-2630\/16\/9\/093021","volume":"16","author":"M Backens","year":"2014","unstructured":"Backens, M.: The zx-calculus is complete for stabilizer quantum mechanics. New J. Phys. 16(9), 093021 (2014)","journal-title":"New J. Phys."},{"issue":"10","key":"3_CR6","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., Barrett, C.W., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023). https:\/\/doi.org\/10.1145\/3587692","journal-title":"Commun. ACM"},{"doi-asserted-by":"publisher","unstructured":"Burgholzer, L., Kueng, R., Wille, R.: Random stimuli generation for the verification of quantum circuits. In: Proceedings of the 26th Asia and South Pacific Design Automation Conference, ASPDAC 2021, pp. 767\u2013772. ACM, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3394885.3431590","key":"3_CR7","DOI":"10.1145\/3394885.3431590"},{"doi-asserted-by":"publisher","unstructured":"Chareton, C., Lee, D., Valiron, B., Vilmart, R., Bardin, S., Xu, Z.: Formal methods for quantum algorithms. In: Akleylek, S., Dundua, B. (eds.) Handbook of Formal Analysis and Verification in Cryptography, pp. 319\u2013422. CRC Press (2023). https:\/\/doi.org\/10.1201\/9781003090052-7","key":"3_CR8","DOI":"10.1201\/9781003090052-7"},{"doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L.: Autoq: an automata-based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 139\u2013153. Springer, Cham (2023)","key":"3_CR9","DOI":"10.1007\/978-3-031-37709-9_7"},{"doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591270","key":"3_CR10","DOI":"10.1145\/3591270"},{"doi-asserted-by":"crossref","unstructured":"Cirac, J.I., P\u00e9rez-Garc\u00eda, D., Schuch, N., Verstraete, F.: Matrix product states and projected entangled pair states: Concepts, symmetries, theorems. Rev. Mod. Phys. 93, 045003 (2021)","key":"3_CR11","DOI":"10.1103\/RevModPhys.93.045003"},{"doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment, A., Heurtel, N., Mansfield, S., Perdrix, S., Valiron, B.: LO$${_v}$$-calculus: a graphical language for linear optical quantum circuits. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0241, pp. 35:1\u201335:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.35, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.MFCS.2022.35","key":"3_CR12","DOI":"10.4230\/LIPIcs.MFCS.2022.35"},{"doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment, A., Heurtel, N., Mansfield, S., Perdrix, S., Valiron, B.: A complete equational theory for quantum circuits. In: 38th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, 26\u201329 June 2023, pp. 1\u201313. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175801","key":"3_CR13","DOI":"10.1109\/LICS56636.2023.10175801"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-70583-3_25","volume-title":"Automata, Languages and Programming","author":"B Coecke","year":"2008","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 298\u2013310. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70583-3_25"},{"issue":"4","key":"3_CR15","doi-asserted-by":"publisher","first-page":"043016","DOI":"10.1088\/1367-2630\/13\/4\/043016","volume":"13","author":"B Coecke","year":"2011","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011)","journal-title":"New J. Phys."},{"doi-asserted-by":"crossref","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Math. (Proceedings) 75(5), 381\u2013392 (1972)","key":"3_CR16","DOI":"10.1016\/1385-7258(72)90034-0"},{"doi-asserted-by":"publisher","unstructured":"Dirac, P.A.M.: A new notation for quantum mechanics. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol.\u00a035, pp. 416\u2013418. Cambridge University Press (1939). https:\/\/doi.org\/10.1017\/S0305004100021162","key":"3_CR17","DOI":"10.1017\/S0305004100021162"},{"doi-asserted-by":"publisher","unstructured":"Hadzihasanovic, A.: A diagrammatic axiomatisation for qubit entanglement. In: 2015 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 573\u2013584 (2015). https:\/\/doi.org\/10.1109\/LICS.2015.59","key":"3_CR18","DOI":"10.1109\/LICS.2015.59"},{"doi-asserted-by":"publisher","unstructured":"Hadzihasanovic, A., Ng, K.F., Wang, Q.: Two complete axiomatisations of pure-state qubit quantum computing. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 502\u2013511. Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3209108.3209128","key":"3_CR19","DOI":"10.1145\/3209108.3209128"},{"doi-asserted-by":"publisher","unstructured":"Jeandel, E., Perdrix, S., Vilmart, R.: A complete axiomatisation of the zx-calculus for clifford+t quantum mechanics. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 559\u2013568. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209131","key":"3_CR20","DOI":"10.1145\/3209108.3209131"},{"doi-asserted-by":"publisher","unstructured":"Jeandel, E., Perdrix, S., Vilmart, R.: Diagrammatic reasoning beyond clifford+t quantum mechanics. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 July 2018, pp. 569\u2013578. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209139","key":"3_CR21","DOI":"10.1145\/3209108.3209139"},{"doi-asserted-by":"publisher","unstructured":"Kissinger, A., van\u00a0de Wetering, J.: PyZX: large scale automated diagrammatic reasoning. In: Coecke, B., Leifer, M. (eds.) Proceedings 16th International Conference on Quantum Physics and Logic, Chapman University, Orange, CA, USA., 10\u201314 June 2019. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0318, pp. 229\u2013241. Open Publishing Association (2020). https:\/\/doi.org\/10.4204\/EPTCS.318.14","key":"3_CR22","DOI":"10.4204\/EPTCS.318.14"},{"doi-asserted-by":"publisher","unstructured":"Le, X.B., Lin, S.W., Sun, J., Sanan, D.: A quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498697","key":"3_CR23","DOI":"10.1145\/3498697"},{"unstructured":"Lewis, M., Soudjani, S., Zuliani, P.: Formal verification of quantum programs: theory, tools and challenges. CoRR abs\/2110.01320 (2021), https:\/\/arxiv.org\/abs\/2110.01320","key":"3_CR24"},{"unstructured":"Li, L., et al.: Qafny: a quantum-program verifier (2024). https:\/\/arxiv.org\/abs\/2211.06411","key":"3_CR25"},{"unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press (2010)","key":"3_CR26"},{"issue":"3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/JETCAS.2022.3202204","volume":"12","author":"T Peham","year":"2022","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the zx-calculus. IEEE J. Emerg. Sel. Top. Circ. Syst. 12(3), 662\u2013675 (2022). https:\/\/doi.org\/10.1109\/JETCAS.2022.3202204","journal-title":"IEEE J. Emerg. Sel. Top. Circ. Syst."},{"unstructured":"Perez-Garcia, D., Verstraete, F., Wolf, M.M., Cirac, J.I.: Matrix product state representations (2007), https:\/\/arxiv.org\/abs\/quant-ph\/0608197","key":"3_CR28"},{"doi-asserted-by":"publisher","unstructured":"Po\u00f3r, B., Wang, Q., Shaikh, R.A., Yeh, L., Yeung, R., Coecke, B.: Completeness for arbitrary finite dimensions of zxw-calculus, a unifying calculus. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201314 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175672","key":"3_CR29","DOI":"10.1109\/LICS56636.2023.10175672"},{"doi-asserted-by":"publisher","unstructured":"Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290346","key":"3_CR30","DOI":"10.1145\/3290346"},{"unstructured":"van\u00a0de Wetering, J.: Zx-calculus for the working quantum computer scientist (2020), https:\/\/arxiv.org\/abs\/2012.13966","key":"3_CR31"},{"doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: Egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434304","key":"3_CR32","DOI":"10.1145\/3434304"},{"doi-asserted-by":"publisher","unstructured":"Xu, Y., Barthe, G., Zhou, L.: Automating equational proofs in dirac notation. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704878","key":"3_CR33","DOI":"10.1145\/3704878"},{"doi-asserted-by":"publisher","unstructured":"Yan, P., Jiang, H., Yu, N.: On incorrectness logic for quantum programs. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527316","key":"3_CR34","DOI":"10.1145\/3527316"},{"issue":"1","key":"3_CR35","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s00236-024-00472-w","volume":"62","author":"S Zhong","year":"2024","unstructured":"Zhong, S.: Birkhoff-von neumann quantum logic enriched with entanglement quantifiers: coincidence theorem and semantic consequence. Acta Informatica 62(1), 7 (2024)","journal-title":"Acta Informatica"},{"doi-asserted-by":"publisher","unstructured":"Zhou, L., Barthe, G., Hsu, J., Ying, M., Yu, N.: A quantum interpretation of bunched logic & quantum separation logic. In: 36th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pp. 1\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470673","key":"3_CR36","DOI":"10.1109\/LICS52264.2021.9470673"},{"doi-asserted-by":"publisher","unstructured":"Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: CoqQ: foundational verification of quantum programs. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571222","key":"3_CR37","DOI":"10.1145\/3571222"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:54:28Z","timestamp":1760086468000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This research was supported by the National Key R&D Program of China under Grant No. 2023YFA1009403.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}