A Logic for Formal Verification of Quantum Programs

Abstract. This paper provides a Hoare-style logic for quantum computation. While the usual Hoare logic helps us to verify classical deterministic programs, our logic supports quantum probabilistic programs. Our target programming language is QPL defined by Selinger, and our logic is an extension of the probabilistic Hoare-style logic defined by den Hartog. In this paper, we demonstrate how the quantum Hoare-style logic proves properties of well-known algorithms.

• Type: Conference
• Year: 2009
• Where: ASIAN
• Authors: Yoshihiko Kakutani
• Keywords: Algorithms, ASIAN 2009, Hoare-style Logic, Logic, Logic Supports Quantum