### 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

- Computer science/Programming languages/Logics
- Computer science/Semantics and reasoning

### Session QHLProver

- Complex_Matrix
- Matrix_Limit
- Quantum_Program
- Partial_State
- Gates
- Quantum_Hoare
- Grover

### Depends on

- Expressiveness of Deep Learning
- Matrices, Jordan Normal Forms, and Spectral Radius Theory

### Used by

- Uncertainty Principle
- Quantum projective measurements and the CHSH inequality

### Auto-related entries

- A Formal Development of a Polychronous Polytimed Coordination Language
- A shallow embedding of HyperCTL*
- The Correctness of Launchbury’s Natural Semantics for Lazy Evaluation

## Cite

×

QHLProver-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Mar 25, 2019 : Isabelle2018