|
Quantum
Hoare
Logic
Title: |
Quantum Hoare Logic |
Authors:
|
Junyi Liu,
Bohua Zhan,
Shuling Wang,
Shenggang Ying,
Tao Liu,
Yangjia Li,
Mingsheng Ying and
Naijun Zhan
|
Submission date: |
2019-03-24 |
Abstract: |
We formalize quantum Hoare logic as given in [1]. In particular, we
specify the syntax and denotational semantics of a simple model of
quantum programs. Then, we write down the rules of quantum Hoare logic
for partial correctness, and show the soundness and completeness of
the resulting proof system. As an application, we verify the
correctness of Grover’s algorithm. |
BibTeX: |
@article{QHLProver-AFP,
author = {Junyi Liu and Bohua Zhan and Shuling Wang and Shenggang Ying and Tao Liu and Yangjia Li and Mingsheng Ying and Naijun Zhan},
title = {Quantum Hoare Logic},
journal = {Archive of Formal Proofs},
month = mar,
year = 2019,
note = {\url{http://isa-afp.org/entries/QHLProver.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Deep_Learning, Jordan_Normal_Form |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|