{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T18:52:16Z","timestamp":1770144736433,"version":"3.49.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001459","name":"Ministry of Education, Singapore","doi-asserted-by":"crossref","award":["MOE2018- T2-1-068"],"award-info":[{"award-number":["MOE2018- T2-1-068"]}],"id":[{"id":"10.13039\/501100001459","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":[[2022,1,16]]},"abstract":"<jats:p>It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch\u2013Jozsa\u2019s algorithm and Grover's algorithm.<\/jats:p>","DOI":"10.1145\/3498697","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic"],"prefix":"10.1145","volume":"6","author":[{"given":"Xuan-Bach","family":"Le","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore"}]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"A preview of Bristlecone Google\u2019s new quantum processor. https:\/\/ai.googleblog.com\/2018\/03\/a-preview-of-bristlecone-googles-new.html.  A preview of Bristlecone Google\u2019s new quantum processor. https:\/\/ai.googleblog.com\/2018\/03\/a-preview-of-bristlecone-googles-new.html."},{"key":"e_1_2_2_2_1","unstructured":"Google Cirq. https:\/\/github.com\/quantumlib\/Cirq.  Google Cirq. https:\/\/github.com\/quantumlib\/Cirq."},{"key":"e_1_2_2_3_1","unstructured":"IBM Q Devices and Simulators. https:\/\/www.research.ibm.com\/ibm-q\/technology\/devices\/.  IBM Q Devices and Simulators. https:\/\/www.research.ibm.com\/ibm-q\/technology\/devices\/."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539796300933"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_6_1","volume-title":"Open quantum assembly language. https:\/\/arxiv.org\/abs\/1707.03429v2","author":"Cross Andrew W.","year":"2017","unstructured":"Andrew W. Cross , Lev S. Bishop , John A. Smolin , and Jay M. Gambetta . Open quantum assembly language. https:\/\/arxiv.org\/abs\/1707.03429v2 , 2017 . Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language. https:\/\/arxiv.org\/abs\/1707.03429v2, 2017."},{"key":"e_1_2_2_7_1","volume-title":"Rapid solution of problems by quantum computation","author":"Deutsch D","year":"1992","unstructured":"D Deutsch and R Jozsa . Rapid solution of problems by quantum computation . 1992 . D Deutsch and R Jozsa. Rapid solution of problems by quantum computation. 1992."},{"key":"e_1_2_2_8_1","first-page":"342","volume-title":"PLDI","author":"Green Alexander S.","year":"2013","unstructured":"Alexander S. Green , Peter LeFanu Lumsdaine , Neil J. Ross , Peter Selinger , and Beno\u00eet Valiron . Quipper : A scalable quantum programming language . In PLDI , pages 333\u2013 342 , 2013 . Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Beno\u00eet Valiron. Quipper: A scalable quantum programming language. In PLDI, pages 333\u2013342, 2013."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_2_12_1","volume-title":"POPL","author":"Li Yangjia","year":"2017","unstructured":"Yangjia Li and Mingsheng Ying . Algorithmic analysis of termination problems for quantum programs . In POPL , 2017 . Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. In POPL, 2017."},{"key":"e_1_2_2_13_1","first-page":"207","volume-title":"CAV","author":"Liu Junyi","year":"2019","unstructured":"Junyi Liu , Bohua Zhan , Shuling Wang , Shenggang Ying , Tao Liu , Yangjia Li , Mingsheng Ying , and Naijun Zhan . Formal Verification of Quantum Algorithms Using Quantum Hoare Logic . In CAV , pages 187\u2013 207 , 2019 . Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. In CAV, pages 187\u2013207, 2019."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1360\/N112017-00095"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2013.6657075"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2505466"},{"key":"e_1_2_2_19_1","first-page":"858","volume-title":"POPL","author":"Paykin Jennifer","year":"2017","unstructured":"Jennifer Paykin , Robert Rand , and Steve Zdancewic . QWIRE : A Core Language for Quantum Circuits . In POPL , pages 846\u2013 858 , 2017 . Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: A Core Language for Quantum Circuits. In POPL, pages 846\u2013858, 2017."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-01-31-49"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_2_24_1","unstructured":"Dave Wecker Krysta M. Svore and Krysta M. Svore. LIQUi|\u3009: A Software Design Architecture and Domain-Specific Language for Quantum Computing. http:\/\/research.microsoft.com\/en-us\/projects\/liquid\/.  Dave Wecker Krysta M. Svore and Krysta M. Svore. LIQUi|\u3009: A Software Design Architecture and Domain-Specific Language for Quantum Computing. http:\/\/research.microsoft.com\/en-us\/projects\/liquid\/."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1038\/299802a0"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_28"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0465-3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498697","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498697"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":28,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498697"],"URL":"https:\/\/doi.org\/10.1145\/3498697","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}