{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:24:47Z","timestamp":1770283487663,"version":"3.49.0"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Quantum computation is inevitably subject to imperfections in its implementation. These imperfections arise from various sources, including environmental noise at the hardware level and the introduction of approximate implementations by quantum algorithm designers, such as lower-depth computations. Given the significant advantage of relational logic in program reasoning and the importance of assessing the robustness of quantum programs between their ideal specifications and imperfect implementations, we design a proof system to verify the approximate relational properties of quantum programs. We demonstrate the effectiveness of our approach by providing the first formal verification of the renowned low-depth approximation of the quantum Fourier transform. Furthermore, we validate the approximate correctness of the repeat-until-success algorithm. From the technical point of view, we develop approximate quantum coupling as a fundamental tool to study approximate relational reasoning for quantum programs, a novel generalization of the widely used approximate probabilistic coupling in probabilistic programs, answering a previously posed open question for projective predicates.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_22","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"495-519","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Approximate Relational Reasoning for\u00a0Quantum Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2930-7447","authenticated-orcid":false,"given":"Peng","family":"Yan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5965-1209","authenticated-orcid":false,"given":"Hanru","family":"Jiang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1188-3032","authenticated-orcid":false,"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"22_CR1","unstructured":"Abhari, A.J., et al.: Scaffold: quantum programming language. Princeton University NJ Department of Computer Science, Tech. rep. (2012)"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Aharonov, D., Kitaev, A., Nisan, N.: Quantum circuits with mixed states (1998). https:\/\/doi.org\/10.48550\/ARXIV.QUANT-PH\/9806029, https:\/\/arxiv.org\/abs\/quant-ph\/9806029","DOI":"10.48550\/ARXIV.QUANT-PH\/9806029"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Aharonov, D., Kitaev, A., Nisan, N.: Quantum circuits with mixed states. In: Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, pp. 20-30. STOC \u201998, Association for Computing Machinery, New York, NY, USA (1998). https:\/\/doi.org\/10.1145\/276698.276708","DOI":"10.1145\/276698.276708"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Aleksandrowicz, G., et\u00a0al.: Qiskit: an open-source framework for quantum computing (2019). https:\/\/doi.org\/10.5281\/zenodo.2562111","DOI":"10.5281\/zenodo.2562111"},{"key":"22_CR5","doi-asserted-by":"publisher","unstructured":"Anil\u00a0Kumar, V., Ramesh, H.: Coupling vs. conductance for the jerrum-sinclair chain*. Random Struct. Algorithms 18(1), 1\u201317 (2001). https:\/\/doi.org\/10.1002\/1098-2418(200101)18:11::AID-RSA13.0.CO;2-7","DOI":"10.1002\/1098-2418(200101)18:11::AID-RSA13.0.CO;2-7"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"Badihi, S., Akinotcho, F., Li, Y., Rubin, J.: ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code. In: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 13\u201324. ESEC\/FSE 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3368089.3409757","DOI":"10.1145\/3368089.3409757"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella\u00a0B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 90\u2013101. POPL \u201909, Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Barthe, G., Hsu, J., Ying, M., Yu, N., Zhou, L.: Relational proofs for quantum programs. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371089","DOI":"10.1145\/3371089"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella-B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst. 35(3) (2013). https:\/\/doi.org\/10.1145\/2492061","DOI":"10.1145\/2492061"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14\u201325. POPL \u201904, Association for Computing Machinery, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Bergstra, J., Tiuryn, J., Tucker, J.: Floyd\u2019s principle, correctness theories and program equivalence. Theor. Comput. Sci. 17(2), 113\u2013149 (1982). https:\/\/doi.org\/10.1016\/0304-3975(82)90001-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397582900019","DOI":"10.1016\/0304-3975(82)90001-9"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Birkhoff, G., Neumann, J.V.: The logic of quantum mechanics. Ann. Math. 37(4), 823\u2013843 (1936). http:\/\/www.jstor.org\/stable\/1968621","DOI":"10.2307\/1968621"},{"key":"22_CR13","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.114.080502","volume":"114","author":"A Bocharov","year":"2015","unstructured":"Bocharov, A., Roetteler, M., Svore, K.M.: Efficient synthesis of universal repeat-until-success quantum circuits. Phys. Rev. Lett. 114, 080502 (2015). https:\/\/doi.org\/10.1103\/PhysRevLett.114.080502","journal-title":"Phys. Rev. Lett."},{"key":"22_CR14","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","DOI":"10.1145\/3591270"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Churchill, B., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1027\u20131040. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314596","DOI":"10.1145\/3314221.3314596"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Cleve, R., Watrous, J.: Fast parallel circuits for the quantum fourier transform. In: Proceedings 41st Annual Symposium on Foundations of Computer Science, pp. 526\u2013536. IEEE Computer Society, Redondo Beach, CA, USA (2000). https:\/\/doi.org\/10.1109\/SFCS.2000.892140","DOI":"10.1109\/SFCS.2000.892140"},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Coppersmith, D.: An approximate fourier transform useful in quantum factoring (2002). https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0201067","DOI":"10.48550\/arxiv.quant-ph\/0201067"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Cousineau, G., Enjalbert, P.: Program equivalence and provability. In: Be\u010dv\u00e1\u0159, J. (ed.) Mathematical Foundations of Computer Science, pp. 237\u2013245. Springer, Berlin, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09526-8_20","DOI":"10.1007\/3-540-09526-8_20"},{"key":"22_CR19","doi-asserted-by":"publisher","unstructured":"Developers, C.: Cirq (2021). https:\/\/doi.org\/10.5281\/zenodo.5182845, See full list of authors on Github: https:\/\/github.com\/quantumlib\/Cirq\/graphs\/contributors","DOI":"10.5281\/zenodo.5182845"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. SIGPLAN Not. 48(6), 333\u2013342 (2013). https:\/\/doi.org\/10.1145\/2499370.2462177","DOI":"10.1145\/2499370.2462177"},{"key":"22_CR21","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502","volume":"103","author":"AW Harrow","year":"2009","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Phys. Rev. Lett. 103, 150502 (2009). https:\/\/doi.org\/10.1103\/PhysRevLett.103.150502","journal-title":"Phys. Rev. Lett."},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Heim, B., et al.: Quantum programming languages. Nat. Rev. Phys. 2, 709\u2013722 (2020). https:\/\/doi.org\/10.1038\/s42254-020-00245-7","DOI":"10.1038\/s42254-020-00245-7"},{"key":"22_CR23","doi-asserted-by":"publisher","unstructured":"Hietala, K., Rand, R., Hung, S.H., Wu, X., Hicks, M.: A verified optimizer for quantum circuits. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434318","DOI":"10.1145\/3434318"},{"key":"22_CR24","unstructured":"Hsu, J.: Probabilistic couplings for probabilistic reasoning (2017)"},{"key":"22_CR25","doi-asserted-by":"publisher","unstructured":"Huang, Y., Martonosi, M.: Statistical assertions for validating patterns and finding bugs in quantum programs. In: Proceedings of the 46th International Symposium on Computer Architecture, pp. 541\u2013553. ISCA \u201919, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3307650.3322213","DOI":"10.1145\/3307650.3322213"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Hung, S., Hietala, K., Zhu, S., Ying, M., Hicks, M., Wu, X.: Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang. 3(POPL), 31:1\u201331:29 (2019). https:\/\/doi.org\/10.1145\/3290344","DOI":"10.1145\/3290344"},{"key":"22_CR27","doi-asserted-by":"publisher","unstructured":"Kakutani, Y.: A logic for formal verification of quantum programs. In: Proceedings of the 13th Asian Conference on Advances in Computer Science: Information Security and Privacy, pp. 79\u201393. ASIAN\u201909, Springer-Verlag, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10622-4_7","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"22_CR28","doi-asserted-by":"publisher","unstructured":"Kitaev, A.Y., Shen, A.H., Vyalyi, M.N.: Classical and Quantum Computation. American Mathematical Society, USA (2002). https:\/\/doi.org\/10.1090\/gsm\/047","DOI":"10.1090\/gsm\/047"},{"key":"22_CR29","unstructured":"Kitaev, A.Y.: Quantum measurements and the abelian stabilizer problem. Electron. Colloquium Comput. Complex. TR96-003 (1996). https:\/\/eccc.weizmann.ac.il\/eccc-reports\/1996\/TR96-003\/index.html"},{"key":"22_CR30","doi-asserted-by":"publisher","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. SIGPLAN Not. 44(6), 327\u2013337 (2009). https:\/\/doi.org\/10.1145\/1543135.1542513","DOI":"10.1145\/1543135.1542513"},{"key":"22_CR31","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Sinha, R., Hawblitzel, C.: Automatic root causing for program equivalence failures in binaries. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 362\u2013379. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_21","DOI":"10.1007\/978-3-319-21690-4_21"},{"key":"22_CR32","doi-asserted-by":"publisher","unstructured":"Li, G., Zhou, L., Yu, N., Ding, Y., Ying, M., Xie, Y.: Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang. 4(OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428218","DOI":"10.1145\/3428218"},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Li, Y., Unruh, D.: Quantum relational hoare logic with expectations. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0198, pp. 136:1\u2013136:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.136, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/14205","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"issue":"9","key":"22_CR34","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1038\/nphys3029","volume":"10","author":"S Lloyd","year":"2014","unstructured":"Lloyd, S., Mohseni, M., Rebentrost, P.: Quantum principal component analysis. Nat. Phys. 10(9), 631\u2013633 (2014). https:\/\/doi.org\/10.1038\/nphys3029","journal-title":"Nat. Phys."},{"issue":"4","key":"22_CR35","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/s00165-014-0319-6","volume":"27","author":"D Lucanu","year":"2015","unstructured":"Lucanu, D., Rusu, V.: Program equivalence by circular reasoning. Form. Asp. Comput. 27(4), 701\u2013726 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0319-6","journal-title":"Form. Asp. Comput."},{"key":"22_CR36","doi-asserted-by":"publisher","unstructured":"Ming, J., Zhang, F., Wu, D., Liu, P., Zhu, S.: Deviation-based obfuscation-resilient program equivalence checking with application to software plagiarism detection. IEEE Trans Reliab. 65(4), 1647\u20131664 (2016). https:\/\/doi.org\/10.1109\/TR.2016.2570554","DOI":"10.1109\/TR.2016.2570554"},{"issue":"5","key":"22_CR37","doi-asserted-by":"publisher","DOI":"10.1063\/1.5019322","volume":"59","author":"I Nechita","year":"2018","unstructured":"Nechita, I., Pucha\u0142a, Z., Pawela, L., \u017byczkowski, K.: Almost all quantum channels are equidistant. J. Math. Phys. 59(5), 052201 (2018). https:\/\/doi.org\/10.1063\/1.5019322","journal-title":"J. Math. Phys."},{"issue":"5","key":"22_CR38","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"GC Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Not. 35(5), 83\u201394 (2000). https:\/\/doi.org\/10.1145\/358438.349314","journal-title":"SIGPLAN Not."},{"key":"22_CR39","doi-asserted-by":"publisher","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, New York, 10th edn. (2011). https:\/\/doi.org\/10.1017\/CBO9780511976667","DOI":"10.1017\/CBO9780511976667"},{"key":"22_CR40","doi-asserted-by":"publisher","unstructured":"Paetznick, A., Svore, K.M.: Repeat-until-success: non-deterministic decomposition of single-qubit unitaries. Quantum Info. Comput. 14(15-16), 1277\u20131301 (2014). https:\/\/doi.org\/10.26421\/QIC14.15-16-2","DOI":"10.26421\/QIC14.15-16-2"},{"key":"22_CR41","doi-asserted-by":"publisher","unstructured":"Pitts, A.: Operationally-Based Theories of Program Equivalence, pp. 241\u2013298. Publications of the Newton Institute, Cambridge University Press, Cambridge (1997). https:\/\/doi.org\/10.1017\/CBO9780511526619.007","DOI":"10.1017\/CBO9780511526619.007"},{"key":"22_CR42","doi-asserted-by":"publisher","unstructured":"Preskill, J.: Quantum computing in the NISQ era and beyond. Quantum 2, 79 (2018). https:\/\/doi.org\/10.22331\/q-2018-08-06-79","DOI":"10.22331\/q-2018-08-06-79"},{"key":"22_CR43","unstructured":"Rand, R.: Verification logics for quantum programs (2019)"},{"key":"22_CR44","doi-asserted-by":"publisher","first-page":"119","DOI":"10.4204\/eptcs.266.8","volume":"266","author":"R Rand","year":"2018","unstructured":"Rand, R., Paykin, J., Zdancewic, S.: QWIRE Practice: formal verification of quantum circuits in Coq. Electron. Proc. Theor. Comput. Sci. 266, 119\u2013132 (2018). https:\/\/doi.org\/10.4204\/eptcs.266.8","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"22_CR45","doi-asserted-by":"publisher","unstructured":"Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings of the 35th Annual Symposium on Foundations of Computer Science, pp. 124\u2013134. SFCS \u201994, IEEE Computer Society, USA (1994). https:\/\/doi.org\/10.1109\/SFCS.1994.365700","DOI":"10.1109\/SFCS.1994.365700"},{"key":"22_CR46","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: CFLOBDDs: context-free-language ordered binary decision diagrams (2023)","DOI":"10.1145\/3651157"},{"key":"22_CR47","unstructured":"Smith, R.S., Curtis, M.J., Zeng, W.J.: A practical quantum instruction set architecture (2016). https:\/\/arxiv.org\/abs\/1608.03355"},{"key":"22_CR48","doi-asserted-by":"publisher","unstructured":"Svore, K., et al.: Q#: enabling scalable quantum computing and development with a high-level DSL. In: Proceedings of the Real World Domain Specific Languages Workshop 2018. RWDSL2018, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3183895.3183901","DOI":"10.1145\/3183895.3183901"},{"key":"22_CR49","doi-asserted-by":"publisher","unstructured":"Tao, R., et al.: Giallar: push-button verification for the Qiskit quantum compiler. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 641\u2013656. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523431","DOI":"10.1145\/3519939.3523431"},{"key":"22_CR50","doi-asserted-by":"publisher","unstructured":"Trabesinger, A.: Quantum computing: towards reality. Nature 543, S1 (2017). https:\/\/doi.org\/10.1038\/543S1a","DOI":"10.1038\/543S1a"},{"key":"22_CR51","doi-asserted-by":"publisher","unstructured":"Unruh, D.: Quantum relational Hoare logic. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290346","DOI":"10.1145\/3290346"},{"key":"22_CR52","doi-asserted-by":"publisher","unstructured":"Voichick, F., Li, L., Rand, R., Hicks, M.: Qunity: a unified language for quantum and classical computing. Proc. ACM Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571225","DOI":"10.1145\/3571225"},{"key":"22_CR53","unstructured":"Watrous, J.: Simpler semidefinite programs for completely bounded norms. Chicago J. Theor. Comput. Sci. 2013, \u00a08 (2013). http:\/\/cjtcs.cs.uchicago.edu\/articles\/2013\/8\/contents.html"},{"key":"22_CR54","doi-asserted-by":"publisher","unstructured":"Weimer, W., Fry, Z.P., Forrest, S.: Leveraging program equivalence for adaptive program repair: models and first results. In: 2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 356\u2013366. ASE \u201913, IEEE Press, Silicon Valley, CA, USA (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693094","DOI":"10.1109\/ASE.2013.6693094"},{"key":"22_CR55","doi-asserted-by":"publisher","unstructured":"Xu, A., Molavi, A., Pick, L., Tannu, S., Albarghouthi, A.: Synthesizing quantum-circuit optimizers. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591254","DOI":"10.1145\/3591254"},{"key":"22_CR56","doi-asserted-by":"publisher","unstructured":"Xu, M., et al.: Quartz: superoptimization of quantum circuits. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 625\u2013640. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3519939.3523433","DOI":"10.1145\/3519939.3523433"},{"key":"22_CR57","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","DOI":"10.1145\/3527316"},{"key":"22_CR58","doi-asserted-by":"publisher","unstructured":"Yang, H.: Relational separation logic. Theor. Comput. Sci. 375(1), 308\u2013334 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.036, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397506009261, festschrift for John C. Reynolds\u2019s 70th birthday","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"22_CR59","doi-asserted-by":"publisher","unstructured":"Ying, M.: Floyd\u2013Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6) (2012). https:\/\/doi.org\/10.1145\/2049706.2049708","DOI":"10.1145\/2049706.2049708"},{"key":"22_CR60","doi-asserted-by":"publisher","unstructured":"Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edn. (2016). https:\/\/doi.org\/10.1016\/C2014-0-02660-3","DOI":"10.1016\/C2014-0-02660-3"},{"key":"22_CR61","doi-asserted-by":"publisher","unstructured":"Ying, M., Duan, R., Feng, Y., Ji, Z.: Predicate Transformer Semantics of Quantum Programs, pp. 311\u2013360. Cambridge University Press, Cambridge (2009). https:\/\/doi.org\/10.1017\/CBO9781139193313.009","DOI":"10.1017\/CBO9781139193313.009"},{"key":"22_CR62","doi-asserted-by":"publisher","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542\u2013558. PLDI 2021, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454061","DOI":"10.1145\/3453483.3454061"},{"key":"22_CR63","doi-asserted-by":"publisher","unstructured":"Yuan, C., McNally, C., Carbin, M.: Twist: sound reasoning for purity and entanglement in quantum programs. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498691","DOI":"10.1145\/3498691"},{"key":"22_CR64","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: Proceedings of the 36th Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS \u201921, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470673","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"22_CR65","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","DOI":"10.1145\/3571222"},{"key":"22_CR66","doi-asserted-by":"publisher","unstructured":"Zhou, L., Yu, N., Ying, M.: An applied quantum Hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1149\u20131162. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314584","DOI":"10.1145\/3314221.3314584"},{"key":"22_CR67","doi-asserted-by":"publisher","unstructured":"Zhou, L., Yu, N., Ying, S., Ying, M.: Quantum earth mover\u2019s distance, a no-go quantum Kantorovich-Rubinstein theorem, and quantum marginal problem. J. Math. Phys. 63(10), 102201 (2022). https:\/\/doi.org\/10.1063\/5.0068344","DOI":"10.1063\/5.0068344"}],"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-65633-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:07:40Z","timestamp":1721891260000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_22","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":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}