Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916613252448256 |
|---|---|
| author | Wu, Huiling Deng, Yuxin Xu, Ming |
| author_facet | Wu, Huiling Deng, Yuxin Xu, Ming |
| contents | Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2308_04741 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs Wu, Huiling Deng, Yuxin Xu, Ming Programming Languages Quantum Physics F.3.1, F.3.2 Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs. |
| title | Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs |
| topic | Programming Languages Quantum Physics F.3.1, F.3.2 |
| url | https://arxiv.org/abs/2308.04741 |