Quantum Hoare Type Theory: Extended Abstract

As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for sim-ilar techniques in the quantum regime. Inspired by Hoare Type Theory [NMB08] in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad [AG09] by in-dexing it with pre-and postconditions that serve as program specifications. In this paper, we intro-duce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples.QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.1