Quantum Hoare Type Theory: Extended Abstract

Kartik Singhal
(University of Chicago)
John Reppy
(University of Chicago)

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.

In Benoît Valiron, Shane Mansfield, Pablo Arrighi and Prakash Panangaden: Proceedings 17th International Conference on Quantum Physics and Logic (QPL 2020), Paris, France, June 2 - 6, 2020, Electronic Proceedings in Theoretical Computer Science 340, pp. 291–302.
See expanded version at https://arxiv.org/abs/2012.02154
Published: 6th September 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.340.15 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org