Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/164233
Title: A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic
Authors: Le, Xuan-Bach
Lin, Shang-Wei
Sun, Jun
Sanan, David
Keywords: Engineering::Computer science and engineering
Issue Date: 2022
Source: 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
Project: MOE2018- T2-1-068 
MOET32020-0004 
Journal: Proceedings of the ACM on Programming Languages 
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.
URI: https://hdl.handle.net/10356/164233
ISSN: 2475-1421
DOI: 10.1145/3498697
Schools: School of Computer Science and Engineering 
Rights: © 2022 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Journal Articles

Files in This Item:
File Description SizeFormat 
3498697.pdf335.74 kBAdobe PDFThumbnail
View/Open

SCOPUSTM   
Citations 50

4
Updated on Feb 16, 2024

Web of ScienceTM
Citations 50

3
Updated on Oct 24, 2023

Page view(s)

84
Updated on Feb 21, 2024

Download(s)

19
Updated on Feb 21, 2024

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.