Publication Type

Journal Article

Version

publishedVersion

Publication Date

1-2022

Abstract

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–Jozsa’s algorithm and Grover's algorithm.

Keywords

Formal Semantics, Quantum Computing, Verification

Discipline

Software Engineering | Theory and Algorithms

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the ACM on Programming Languages

Volume

6

Issue

POPL

First Page

1

Last Page

27

Identifier

10.1145/3498697

Publisher

ACM

Copyright Owner and License

Authors

Creative Commons License

Creative Commons Attribution 4.0 International License
This work is licensed under a Creative Commons Attribution 4.0 International License.

Additional URL

https://doi.org/10.1145/3498697

Share

COinS