{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:32Z","timestamp":1780994792864,"version":"3.54.1"},"reference-count":67,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470673","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T20:14:07Z","timestamp":1625688847000},"page":"1-14","source":"Crossref","is-referenced-by-count":20,"title":["A Quantum Interpretation of Bunched Logic & Quantum Separation Logic"],"prefix":"10.1109","author":[{"given":"Li","family":"Zhou","sequence":"first","affiliation":[{"name":"Max Planck Institute for Security and Privacy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin–Madison"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"ref33","author":"ying","year":"2016","journal-title":"Foundations of Quantum Programming"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"1829","DOI":"10.1103\/PhysRevA.59.1829","article-title":"Quantum secret sharing","volume":"59","author":"hillery","year":"1999","journal-title":"Phys Rev A"},{"key":"ref37","article-title":"Quantum abstract interpretation","author":"yu","year":"2021","journal-title":"Proceedings of the 42th ACM SIGPLAN Conference on Programming Language Design and Implementation ser PLDI 2021"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"ref35","first-page":"311","article-title":"Predicate transformer semantics of quantum programs","author":"ying","year":"2010","journal-title":"Semantic Techniques in Quantum Computation"},{"key":"ref34","doi-asserted-by":"crossref","DOI":"10.1109\/LICS52264.2021.9470673","article-title":"A quantum interpretation of bunched logic for quantum separation logic","author":"zhou","year":"2021"},{"key":"ref60","article-title":"Alternation in quantum programming: From superposition of data to superposition of programs","author":"ying","year":"2014"},{"key":"ref62","article-title":"Topological obstructions to implementing controlled unknown unitaries","author":"gavorov\u00e1","year":"2020"},{"key":"ref61","first-page":"33","article-title":"Quantum alternation: Prospects and problems","volume":"195","author":"b?descu","year":"0"},{"key":"ref28","article-title":"Private quantum channels and the cost of randomizing quantum information","author":"mosca","year":"2000"},{"key":"ref63","article-title":"Weakly measured while loops: peeking at quantum states","author":"andr\u00e9s-mart\u00ednez","year":"2021"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.67.042317"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1142\/S0217979213450197"},{"key":"ref65","first-page":"173","author":"plenio","year":"2014","journal-title":"An Introduction to Entanglement Theory"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.83.648"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/16\/1\/013009"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000444"},{"key":"ref2","volume":"26","author":"pym","year":"2002","journal-title":"The semantics and proof theory of the logic of bunched implications ser Applied Logic Series"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The logic of bunched implications","volume":"5","author":"o\u2019hearn","year":"1999","journal-title":"The Bulletin of Symbolic Logic"},{"key":"ref20","article-title":"Proving quantum programs correct","author":"hietala","year":"2020"},{"key":"ref22","author":"nielsen","year":"2002","journal-title":"Quantum Computation and Quantum Information"},{"key":"ref21","article-title":"An introduction to separation logic (preliminary draft)","author":"reynolds","year":"2008","journal-title":"Course notes October"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"ref23","article-title":"Reasoning about parallel quantum programs","author":"ying","year":"2018"},{"key":"ref26","article-title":"quantumlib\/Cirq: A Python framework for creating, editing, and invoking noisy intermediate scale quantum (NISQ) circuits","year":"2018"},{"key":"ref25","article-title":"Certified quantum computation in Isabelle\/HOL","author":"bordg","year":"2020","journal-title":"Journal of Automated Reasoning"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"ref51","article-title":"Verification logics for quantum programs","author":"rand","year":"2016"},{"key":"ref59","article-title":"Defining quantum control flow","author":"ying","year":"2012"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"ref57","article-title":"Routed quantum circuits","author":"vanrietvelde","year":"2020"},{"key":"ref56","article-title":"Quantum Hoare type theory","author":"singhal","year":"2020"},{"key":"ref55","article-title":"Quantum Hoare type theory: Extended abstract","author":"singhal","year":"0"},{"key":"ref54","article-title":"Quantum relational Hoare logic with expectations","author":"li","year":"2019"},{"key":"ref53","article-title":"Quantum temporal logic","author":"yu","year":"2019"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.02.008"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/MARK.1979.8817296"},{"key":"ref11","article-title":"Bunched logics: a uniform approach","author":"docherty","year":"2019","journal-title":"Ph D Dissertation"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1038\/nature23474"},{"key":"ref13","article-title":"TensorFlow Quantum: A software framework for quantum machine learning","author":"broughton","year":"2020"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1038\/ncomms5213"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/18\/2\/023023"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.8"},{"key":"ref19","article-title":"A verified optimizer for quantum circuits","volume":"5","author":"hietala","year":"2021"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"ref5","first-page":"1","author":"o\u2019hearn","year":"2001","journal-title":"Computer Science Logic"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","article-title":"A semantics for concurrent separation logic","volume":"375","author":"brookes","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"o\u2019hearn","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"ref9","article-title":"A probabilistic separation logic","volume":"4","author":"barthe","year":"2019","journal-title":"Proc ACM Program Lang"},{"key":"ref46","first-page":"39","article-title":"The logic of quantum programs","author":"baltag","year":"0"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"ref42","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1103\/PhysRevA.59.162","article-title":"Quantum entanglement for secret sharing and secret splitting","volume":"59","author":"karlsson","year":"1999","journal-title":"Phys Rev A"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/359168.359176"},{"key":"ref44","article-title":"The logic of quantum program verification","author":"akatov","year":"2005","journal-title":"Master’s thesis"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-020-00245-7"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Rome, Italy","start":{"date-parts":[[2021,6,29]]},"end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470673.pdf?arnumber=9470673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T07:31:27Z","timestamp":1672731087000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470673\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":67,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470673","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}