Quantum Hoare Type Theory: Extended Abstract

TL;DR

This paper introduces Quantum Hoare Type Theory (QHTT), a formal system extending quantum programming with specifications to improve correctness and reasoning, inspired by classical Hoare Type Theory.

Contribution

It proposes the first formal type system for quantum programs that incorporates pre- and post-conditions, enabling verification and reasoning about quantum code.

Findings

Introduces syntax and typing rules for QHTT

Demonstrates effectiveness with example quantum programs

Lays groundwork for a unified quantum programming and verification system

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 similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce 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.