Quantum Hoare Logic

Junyi Liu, Bohua Zhan 🌐, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan

March 24, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session QHLProver

Depends on

Used by

Cite

× 
@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   = {March},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/QHLProver.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: