Reasoning About Imperative Quantum Programs
Reasoning About Imperative Quantum Programs
Chadha, Mateus, and Sernadas study logical reasoning for imperative quantum programs and its connection to probabilistic-program methods.
Paper information (2006, Electronic Notes in Theoretical Computer Science 158:19–39) — Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. DOI
Work
The paper studies how to reason about programs with quantum operations, classical control, and imperative structure. It places state transformation, probabilistic observations, and Hoare-style program logic in one discussion, and analyzes the semantics and provable properties of imperative quantum programs. It also relates the problem to probabilistic programs, quantum propositional logic, and quantum-protocol research.
Contributions
- A formal reasoning perspective for the states and control structures of imperative quantum programs.
- An account of connections between quantum-program semantics, probabilistic predicates, and Hoare-style logic.
- A compositional setting for analyzing quantum operations, classical commands, and program properties.
- An early reference point for later quantum-program verification, quantum Hoare logic, and quantitative reasoning.
Limits
The paper studies an abstract program model and logic; it does not verify a particular compiler, chip, or complete software system. Proofs depend on the chosen state space, observation language, termination convention, and probabilistic semantics; noise, floating-point error, dynamic resources, and hardware constraints require separate models. Provability in the logic also does not mean that every program property is automatically decidable.
Connections
Together with Quantum Weakest Preconditions, this paper belongs to the early quantum-program-logic line: it emphasizes reasoning about imperative programs, while the other paper emphasizes predicate transformers derived from state transformations. It also continues the imperative and probabilistic semantics of Quantum Programming and provides background for the wiki's Quantum Hoare Logic and verification-tools entries. Compared with Communicating Quantum Processes, it focuses on assertions about programs rather than interprocess channels.
Original paper
Rohit Chadha, Paulo Mateus, and Amílcar Sernadas, Reasoning About Imperative Quantum Programs, Electronic Notes in Theoretical Computer Science 158, 19–39 (2006), DOI: 10.1016/j.entcs.2006.04.003.