Conference

A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic

Xuan-Bach Le, Shang-Wei Lin, Jun Sun, David Sanan

CORE A*

Venue: POPL 2022 (CORE Rank A*)
Location: Philadelphia, USA
Date: January 2022
Research area: Quantum Reasoning
DOI: 10.1145/3498697

Abstract

Quantum programs are not only complicated to design but also challenging to verify, as quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To address the state-space explosion problem in 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 integrate separation logic into our framework and enable local reasoning via a quantum frame rule analogous to the classical frame rule. For evaluation, we apply our framework to verify representative quantum programs, including Deutsch–Jozsa's algorithm and Grover's algorithm.

Quantum ComputingSeparation LogicProgram Verification

Cite this paper

@inproceedings{le2022quantumsep,
  author    = {Le, Xuan-Bach and Lin, Shang-Wei and Sun, Jun and Sanan, David},
  title     = {A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic},
  booktitle = {Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022)},
  pages     = {1--27},
  publisher = {Association for Computing Machinery},
  year      = {2022},
  doi       = {10.1145/3498697}
}