{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,17]],"date-time":"2026-02-17T11:48:49Z","timestamp":1771328929374,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031659409","type":"print"},{"value":"9783031659416","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-65941-6_5","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:10:56Z","timestamp":1722496256000},"page":"84-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Equivalence Checking of\u00a0Quantum Circuits Based on\u00a0Dirac Notation in\u00a0Maude"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1601-4584","authenticated-orcid":false,"given":"Canh Minh","family":"Do","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,2]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Amy, M., Maslov, D., Mosca, M., Roetteler, M.: A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits. Trans. Comp.-Aided Des. Integr. Circuits Syst. 32(6), 818\u2013830 (2013). https:\/\/doi.org\/10.1109\/TCAD.2013.2244643","DOI":"10.1109\/TCAD.2013.2244643"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Bennett, C.H., Wiesner, S.J.: Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states. Phys. Rev. Lett. 69, 2881\u20132884 (1992). https:\/\/doi.org\/10.1103\/PhysRevLett.69.2881","DOI":"10.1103\/PhysRevLett.69.2881"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40(9), 1810\u20131824 (2021). https:\/\/doi.org\/10.1109\/TCAD.2020.3032630","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All about Maude\u2014a high-performance logical framework: how to specify, program and verify systems in rewriting logic. In: Lecture Notes in Computer Science, vol.\u00a04350. Springer, Berlin (2007).https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Cowtan, A., Dilkes, S., Duncan, R., Krajenbrink, A., Simmons, W., Sivarajah, S.: On the qubit routing problem. In: 14th Conference on the Theory of Quantum Computation, Communication and Cryptography, TQC 2019, 2019, University of Maryland, College Park, Maryland, USA. LIPIcs, vol.\u00a0135, pp. 5:1\u20135:32. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.TQC.2019.5","DOI":"10.4230\/LIPICS.TQC.2019.5"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Dirac, P.A.M.: A new notation for quantum mechanics. Math. Proc. Cambridge Philos. Soc. 35(3), 416\u2013418 (1939). https:\/\/doi.org\/10.1017\/S0305004100021162","DOI":"10.1017\/S0305004100021162"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Do, C.M., Ogata, K.: Symbolic model checking quantum circuits in Maude. In: The 35th International Conference on Software Engineering and Knowledge Engineering, SEKE 2023, pp. 103\u2013108 (2023). https:\/\/doi.org\/10.18293\/SEKE2023-014","DOI":"10.18293\/SEKE2023-014"},{"key":"5_CR8","unstructured":"Do, C.M., Ogata, K.: Theoretical foundation for equivalence checking of quantum circuits. In: The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, FAVPQC 2023 (2023). https:\/\/favpqc2023.gitlab.io\/files\/papers\/6-Canh.pdf"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Garcia-Escartin, J.C., Chamorro-Posada, P.: Equivalent Quantum Circuits (2011). https:\/\/doi.org\/10.48550\/arXiv.1110.2998","DOI":"10.48550\/arXiv.1110.2998"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Giles, B., Selinger, P.: Exact synthesis of multiqubit Clifford+$$T$$ circuits. Phys. Rev. A 87, 032332 (2013). https:\/\/doi.org\/10.1103\/PhysRevA.87.032332","DOI":"10.1103\/PhysRevA.87.032332"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Maslov, D., Dueck, G.W., Miller, D.M., Negrevergne, C.: Quantum circuit simplification and level compaction. Trans. Comp.-Aided Des. Integr. Circuits Syst. 27(3), 436\u2013444 (008). https:\/\/doi.org\/10.1109\/TCAD.2007.911334","DOI":"10.1109\/TCAD.2007.911334"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Maslov, D.: Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization. Phys. Rev. A 93(2) (2016). https:\/\/doi.org\/10.1103\/physreva.93.022311","DOI":"10.1103\/physreva.93.022311"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7), 721\u2013781 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.06.003, rewriting Logic and its Applications","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Nam, Y., Ross, N.J., Su, Y., Childs, A.M., Maslov, D.: Automated optimization of large quantum circuits with continuous parameters. NPJ Quantum Inf. 4(1), 23 (2018). https:\/\/doi.org\/10.1038\/s41534-018-0072-4","DOI":"10.1038\/s41534-018-0072-4"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010). https:\/\/doi.org\/10.1017\/CBO9780511976667","DOI":"10.1017\/CBO9780511976667"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: Qwire: A core language for quantum circuits. SIGPLAN Not. 52(1), 846\u2013858 (2017). https:\/\/doi.org\/10.1145\/3093333.3009894","DOI":"10.1145\/3093333.3009894"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the ZX-calculus. IEEE J. Emerging Sel. Top. Circuits Syst. 12(3), 662\u2013675 (2022).https:\/\/doi.org\/10.1109\/jetcas.2022.3202204","DOI":"10.1109\/jetcas.2022.3202204"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Sasanian, Z., Miller, D.M.: Reversible and quantum circuit optimization: A functional approach. In: Reversible Computation, pp. 112\u2013124. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-36315-3_9","DOI":"10.1007\/978-3-642-36315-3_9"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Shi, W., Cao, Q., Deng, Y., Jiang, H., Feng, Y.: Symbolic reasoning about quantum circuits in Coq. J. Comput. Sci. Technol. 36(6), 1291\u20131306 (2021). https:\/\/doi.org\/10.1007\/s11390-021-1637-9","DOI":"10.1007\/s11390-021-1637-9"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124\u2013134 (1994). https:\/\/doi.org\/10.1109\/SFCS.1994.365700","DOI":"10.1109\/SFCS.1994.365700"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Siraichi, M.Y., Santos, V.F.D., Collange, C., Pereira, F.M.Q.: Qubit allocation. In: Proceedings of the 2018 International Symposium on Code Generation and Optimization, pp. 113\u2013125. CGO 2018, Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3168822","DOI":"10.1145\/3168822"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Takagi, T., Do, C.M., Ogata, K.: Automated quantum program verification in dynamic quantum logic. In: Dynamic Logic. New Trends and Applications, pp. 68\u201384. Springer Nature Switzerland (2024).https:\/\/doi.org\/10.1007\/978-3-031-51777-8_5","DOI":"10.1007\/978-3-031-51777-8_5"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Wille, R., Burgholzer, L., Zulehner, A.: Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations. In: Proceedings of the 56th Annual Design Automation Conference 2019, DAC 2019, p.\u00a0142. ACM, Las Vegas, NV, USA (2019). https:\/\/doi.org\/10.1145\/3316781.3317859","DOI":"10.1145\/3316781.3317859"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Wille, R., Hillmich, S., Burgholzer, L.: Tools for quantum computing based on decision diagrams. ACM Trans. Quantum Comput. 3(3) (2022). https:\/\/doi.org\/10.1145\/3491246","DOI":"10.1145\/3491246"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Zulehner, A., Paler, A., Wille, R.: Efficient mapping of quantum circuits to the IBM QX architectures. In: 2018 Design, Automation & Test in Europe Conference and Exhibition (DATE), pp. 1135\u20131138 (2018). https:\/\/doi.org\/10.23919\/DATE.2018.8342181","DOI":"10.23919\/DATE.2018.8342181"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65941-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T07:11:38Z","timestamp":1722496298000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65941-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031659409","9783031659416"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65941-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wrla2024.gitlab.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}