{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T01:02:05Z","timestamp":1767920525846,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100005683","name":"Kyoto University","doi-asserted-by":"publisher","award":["Hakubi Project"],"award-info":[{"award-number":["Hakubi Project"]}],"id":[{"id":"10.13039\/501100005683","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP24KJ0133"],"award-info":[{"award-number":["JP24KJ0133"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005683","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJSP2110"],"award-info":[{"award-number":["JPMJSP2110"]}],"id":[{"id":"10.13039\/501100005683","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005683","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJAX23CT"],"award-info":[{"award-number":["JPMJAX23CT"]}],"id":[{"id":"10.13039\/501100005683","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.<\/jats:p>","DOI":"10.1145\/3776648","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"144-173","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5208-3106","authenticated-orcid":false,"given":"Yusuke","family":"Matsushita","sequence":"first","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4416-2655","authenticated-orcid":false,"given":"Kengo","family":"Hirata","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"},{"name":"Kyoto University, Kyoto, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-9335","authenticated-orcid":false,"given":"Ryo","family":"Wakizaka","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9179-5827","authenticated-orcid":false,"given":"Emanuele","family":"D'Osualdo","sequence":"additional","affiliation":[{"name":"University of Konstanz, Konstanz, Germany"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704894"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90660-2_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_8"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656419"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_14_1","volume-title":"Fowler and Craig Gidney","author":"Austin","year":"2019","unstructured":"Austin G. Fowler and Craig Gidney. 2019. Low Overhead Quantum Computation Using Lattice Surgery. CoRR, Aug., arxiv:1808.06709. arxiv:1808.06709"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-06-18-74"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_1_17_1","first-page":"7","article-title":"Factoring Using 2n + 2 Qubits with Toffoli Based Modular Multiplication. Quantum Info","volume":"17","author":"H\u00e4ner Thomas","year":"2017","unstructured":"Thomas H\u00e4ner, Martin Roetteler, and Krysta M. Svore. 2017. Factoring Using 2n + 2 Qubits with Toffoli Based Modular Multiplication. Quantum Info. Comput., 17, 7-8 (2017), June, 673\u2013684. issn:1533-7146","journal-title":"Comput."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776731"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704842"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/14\/12\/123011"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_22_1","unstructured":"Mark Koch Agust\u00edn Borgna Craig Roy Alan Lawrence Kartik Singhal Seyon Sivarajah and Ross Duncan. 2025. Imperative Quantum Programming with Ownership and Borrowing in Guppy. CoRR Oct. arxiv:2510.13082. arxiv:2510.13082"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591226"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662135"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158123"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_29_1","unstructured":"Yusuke Matsushita Kengo Hirata Ryo Wakizaka and Emanuele D\u2019Osualdo. 2025. RapunSL: Untangling Quantum Computing with Separation Linear Combination and Mixing. CoRR Dec. arxiv:2511.23472. arxiv:2511.23472"},{"key":"e_1_2_1_30_1","unstructured":"Junhong Nie Wei Zi and Xiaoming Sun. 2024. Quantum Circuit for Multi-Qubit Toffoli Gate with Optimal Resource. CoRR Feb. arxiv:2402.05053. arxiv:2402.05053"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_35_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Sabry Amr","unstructured":"Amr Sabry, Beno\u00eet Valiron, and Juliana Kaizer Vizzotto. 2018. From Symmetric Pattern-Matching to Quantum Control. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham. 348\u2013364. isbn:978-3-319-89366-2"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.52.R2493"},{"key":"e_1_2_1_37_1","unstructured":"Bonan Su Li Zhou Yuan Feng and Mingsheng Ying. 2024. BI-based Reasoning about Quantum Programs with Heap Manipulations. CoRR Sept. arxiv:2409.10153. arxiv:2409.10153"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Unruh Dominique","year":"2021","unstructured":"Dominique Unruh. 2021. Quantum Hoare Logic with Ghost Variables. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE Press, Article 47, 13 pages."},{"key":"e_1_2_1_41_1","unstructured":"Huiling Wu Yuxin Deng and Ming Xu. 2025. Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs. CoRR Feb. arxiv:2308.04741. arxiv:2308.04741"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571222"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649821"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776648","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:02:07Z","timestamp":1767898927000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776648"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776648"],"URL":"https:\/\/doi.org\/10.1145\/3776648","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}