Reasoning About Imperative Quantum Programs

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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Rohit Chadha, Paulo Mateus, Amílcar Sernadas
• Keywords: ENTCS 2006, Logic, Quantum Imperative Programs, Sound Hoare-style Calculus