Sciweavers

Share
ASIAN
2009
Springer

A Logic for Formal Verification of Quantum Programs

10 years 4 months ago
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.
Yoshihiko Kakutani
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2009
Where ASIAN
Authors Yoshihiko Kakutani
Comments (0)
books