| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 423047 | Electronic Notes in Theoretical Computer Science | 2006 | 21 Pages |
Abstract
A logic for reasoning about states of basic quantum imperative programs is presented. The models of the logic are ensembles obtained by attaching probabilities to pairs of quantum states and classical states. The state logic is used to provide a sound Hoare-style calculus for quantum imperative programs. The calculus is illustrated by proving the correctness of the Deutsch algorithm.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
