Foundations of quantum programming

Front Cover; Foundations of Quantum Programming; Copyright; Contents; Preface; Acknowledgments; Part I: Introduction and preliminaries; Chapter 1: Introduction; 1.1 Brief history of quantum programming research; 1.1.1 Design of Quantum Programming Languages; 1.1.2 Semantics of Quantum Programming Languages; 1.1.3 Verification and Analysis of Quantum Programs; 1.2 Approaches to quantum programming; 1.2.1 Superposition-of-Data

Quantum Programs with Classical Control; 1.2.2 Superposition-of-Programs

Quantum Programs with Quantum Control; 1.3 Structure of the Book; Chapter 2: Preliminaries

2.1 Quantum mechanics2.1.1 Hilbert Spaces; 2.1.2 Linear Operators; 2.1.3 Unitary Transformations; 2.1.4 Quantum Measurements; 2.1.5 Tensor Products of Hilbert Spaces; 2.1.6 Density Operators; 2.1.7 Quantum Operations; 2.2 Quantum circuits; 2.2.1 Basic Definitions; 2.2.2 One-Qubit Gates; 2.2.3 Controlled Gates; 2.2.4 Quantum Multiplexor; 2.2.5 Universality of Gates; 2.2.6 Measurement in Circuits; 2.3 Quantum algorithms; 2.3.1 Quantum Parallelism and Interference; 2.3.2 Deutsch-Jozsa Algorithm; 2.3.3 Grover Search Algorithm; 2.3.4 Quantum Walks; 2.3.5 Quantum-Walk Search Algorithm

2.3.6 Quantum Fourier Transform2.3.7 Phase Estimation; 2.4 Bibliographic remarks; Part II: Quantum programswith classicalcontrol; Chapter 3: Syntax and semantics of quantum programs; 3.1 Syntax; 3.2 Operational semantics; 3.3 Denotational semantics; 3.3.1 Basic Properties of Semantic Functions; 3.3.2 Quantum Domains; 3.3.3 Semantic Function of Loop; 3.3.4 Change and Access of Quantum Variables; 3.3.5 Termination and Divergence Probabilities; 3.3.6 Semantic Functions as Quantum Operations; 3.4 Classical recursion in quantum programming; 3.4.1 Syntax; 3.4.2 Operational Semantics

3.4.3 Denotational Semantics3.4.4 Fixed Point Characterization; 3.5 Illustrative example: Grover quantum search; 3.6 Proofs of lemmas; 3.7 Bibliographic remarks; Chapter 4: Logic for quantum programs; 4.1 Quantum predicates; 4.1.1 Quantum Weakest Preconditions; 4.2 Floyd-Hoare logic for quantum programs; 4.2.1 Correctness Formulas; 4.2.2 Weakest Preconditions of Quantum Programs; 4.2.3 Proof System for Partial Correctness; 4.2.4 Proof System for Total Correctness; 4.2.5 An Illustrative Example: Reasoning aboutthe Grover Algorithm; 4.3 Commutativity of quantum weakest preconditions

4.4 Bibliographic remarksChapter 5: Analysis of quantum programs; 5.1 Termination analysis of quantum while-loops; 5.1.1 Quantum while-Loops with Unitary Bodies; 5.1.2 General Quantum while-Loops; 5.1.3 An Example; 5.2 Quantum graph theory; 5.2.1 Basic Definitions; 5.2.2 Bottom Strongly Connected Components; 5.2.3 Decomposition of the State Hilbert Space; 5.3 Reachability analysis of quantum Markov chains; 5.3.1 Reachability Probability; 5.3.2 Repeated Reachability Probability; 5.3.3 Persistence Probability; 5.4 Proofs of technical lemmas; 5.5 Bibliographic remarks