Quantum Hoare Logic (Q7361944)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry QHLProver
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Quantum Hoare Logic |
AFP entry QHLProver |
Statements
24 March 2019
0 references
Junyi Liu
0 references
Bohua Zhan
0 references
Shuling Wang
0 references
Shenggang Ying
0 references
Tao Liu
0 references
Yangjia Li
0 references
Mingsheng Ying
0 references
Naijun Zhan
0 references
Quantum Hoare Logic (English)
0 references
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.
0 references
