Proof rules for purely quantum programs
Programming Languages
2007-05-23 v3 Quantum Physics
Abstract
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.
Cite
@article{arxiv.cs/0507043,
title = {Proof rules for purely quantum programs},
author = {Yuan Feng and Runyao Duan and Zhengfeng Ji and Mingsheng Ying},
journal= {arXiv preprint arXiv:cs/0507043},
year = {2007}
}
Comments
Now 12 pages, introduction and Section 3 rewritten, some errors corrected