Predicate Transformer Semantics of Quantum Programs

Cambridge University Press
Publication Type:
Semantic Techniques in Quantum Computation, 2010, 1, pp. 311 - 360
Issue Date:
Full metadata record
Files in This Item:
Filename Description Size
Thumbnail2008004719.pdf3.37 MB
Adobe PDF
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selingerâs suggestion of representing quantum programs by superoperators and elucidates DâHondt-Panangadenâs theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoffâvon Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal coujunctivity and termination law of quantum programs are proved, and Hoareâs induction rule is established in the quantum setting.
Please use this identifier to cite or link to this item: