Proof rules for purely quantum programs

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a purely quantum language fragment which describes the quantum part of a future quantum computer in Knill's architecture. The denotational semantics, weakest precondition semantics, and weakest liberal precondition semantics of this language fragment are introduced. To help reasoning about quantum programs involving quantum loops, we extend proof rules for classical probabilistic programs to our purely quantum programs.
Now 12 pages, introduction and Section 3 rewritten, some errors corrected

Keywords

Programming Languages, Quantum Physics, D.3.1; F.3.1

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/101854

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0507043
 http://arxiv.org/abs/cs/0507043

Collections

arXiv