Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2022

Abstract

It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our framework and invent the $\hoarule{qframe}$ rule, the quantum counterpart of the frame rule, to support local reasoning of quantum programs. The design of our framework is planned with a mindset for intuition and human-readability, using vectors in Dirac notation for reasoning instead of the orthodox matrix representation as in existing approaches. For evaluation, we apply our framework to verify various quantum programs such as Deutsch-Jozsa’s algorithm and Grover’s algorithm.

Keywords

Quantum Computing, Verification, Formal Semantics

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

POPL '22: Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages, Philadelphia, Virtual, January 16-22

First Page

1

Last Page

27

Publisher

ACM

City or Country

New York

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

Download

Share

COinS