A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic
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...
Saved in:
Main Authors: | , , , |
---|---|
Other Authors: | |
Format: | Article |
Language: | English |
Published: |
2023
|
Subjects: | |
Online Access: | https://hdl.handle.net/10356/164233 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Nanyang Technological University |
Language: | English |
id |
sg-ntu-dr.10356-164233 |
---|---|
record_format |
dspace |
spelling |
sg-ntu-dr.10356-1642332023-01-11T00:18:57Z A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic Le, Xuan-Bach Lin, Shang-Wei Sun, Jun Sanan, David School of Computer Science and Engineering Engineering::Computer science and engineering Quantum Computing Formal Semantics 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. Ministry of Education (MOE) Published version This work is supported by project MOE2018- T2-1-068 and project MOET32020-0004, both are funded by the Singapore Ministry of Education. 2023-01-11T00:18:57Z 2023-01-11T00:18:57Z 2022 Journal Article Le, X., Lin, S., Sun, J. & Sanan, D. (2022). A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic. Proceedings of the ACM On Programming Languages, 6(POPL), 36:1-36:27. https://dx.doi.org/10.1145/3498697 2475-1421 https://hdl.handle.net/10356/164233 10.1145/3498697 2-s2.0-85123194320 POPL 6 36:1 36:27 en MOE2018- T2-1-068 MOET32020-0004 Proceedings of the ACM on Programming Languages © 2022 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License. application/pdf |
institution |
Nanyang Technological University |
building |
NTU Library |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
NTU Library |
collection |
DR-NTU |
language |
English |
topic |
Engineering::Computer science and engineering Quantum Computing Formal Semantics |
spellingShingle |
Engineering::Computer science and engineering Quantum Computing Formal Semantics Le, Xuan-Bach Lin, Shang-Wei Sun, Jun Sanan, David A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
description |
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. |
author2 |
School of Computer Science and Engineering |
author_facet |
School of Computer Science and Engineering Le, Xuan-Bach Lin, Shang-Wei Sun, Jun Sanan, David |
format |
Article |
author |
Le, Xuan-Bach Lin, Shang-Wei Sun, Jun Sanan, David |
author_sort |
Le, Xuan-Bach |
title |
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
title_short |
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
title_full |
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
title_fullStr |
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
title_full_unstemmed |
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
title_sort |
quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic |
publishDate |
2023 |
url |
https://hdl.handle.net/10356/164233 |
_version_ |
1756370557471817728 |