A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
- URL: http://arxiv.org/abs/2102.00329v1
- Date: Sat, 30 Jan 2021 22:24:36 GMT
- Title: A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
- Authors: Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
- Abstract summary: We develop a program logic where pre- and post-conditions are BI formulas describing quantum states.
We exercise the logic for proving the security of quantum one-time pad and secret sharing.
- Score: 22.507329566323982
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We propose a model of the substructural logic of Bunched Implications (BI)
that is suitable for reasoning about quantum states. In our model, the
separating conjunction of BI describes separable quantum states. We develop a
program logic where pre- and post-conditions are BI formulas describing quantum
states -- the program logic can be seen as a counterpart of separation logic
for imperative quantum programs. We exercise the logic for proving the security
of quantum one-time pad and secret sharing, and we show how the program logic
can be used to discover a flaw in Google Cirq's tutorial on the Variational
Quantum Algorithm (VQA).
Related papers
- BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations.
We develop a quantum BI-style logic that includes interpretations for separating implication.
We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
arXiv Detail & Related papers (2024-09-16T10:34:45Z) - Quantum process tomography of continuous-variable gates using coherent
states [49.299443295581064]
We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit.
We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
arXiv Detail & Related papers (2023-03-02T18:08:08Z) - Compilation of algorithm-specific graph states for quantum circuits [55.90903601048249]
We present a quantum circuit compiler that prepares an algorithm-specific graph state from quantum circuits described in high level languages.
The computation can then be implemented using a series of non-Pauli measurements on this graph state.
arXiv Detail & Related papers (2022-09-15T14:52:31Z) - A Quantum Algorithm for Computing All Diagnoses of a Switching Circuit [73.70667578066775]
Faults are by nature while most man-made systems, and especially computers, work deterministically.
This paper provides such a connecting via quantum information theory which is an intuitive approach as quantum physics obeys probability laws.
arXiv Detail & Related papers (2022-09-08T17:55:30Z) - Abstract interpretation, Hoare logic, and incorrectness logic for
quantum programs [6.2147758224415055]
Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs.
We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic.
arXiv Detail & Related papers (2022-06-28T05:49:55Z) - Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum
Programs [1.1878820609988696]
A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs.
In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
arXiv Detail & Related papers (2022-05-04T08:57:44Z) - LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems.
We present a finitary syntax, a relational semantics and a sound proof system for this logic.
As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
arXiv Detail & Related papers (2021-10-04T12:20:23Z) - The Logic of Quantum Programs [77.34726150561087]
We present a logical calculus for reasoning about information flow in quantum programs.
In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
arXiv Detail & Related papers (2021-09-14T16:08:37Z) - PBS-Calculus: A Graphical Language for Coherent Control of Quantum
Computations [77.34726150561087]
We introduce the PBS-calculus to represent and reason on quantum computations involving coherent control of quantum operations.
We equip the language with an equational theory, which is proved to be sound and complete.
We consider applications like the implementation of controlled permutations and the unrolling of loops.
arXiv Detail & Related papers (2020-02-21T16:15:58Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.