2021/09/06 by Kartik Singhal, John Reppy
Computer Science · Physics and Astronomy · #Hoare logic #Logic, programming, and type systems #Monad (category theory) #Quantum #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum computer #Type (biology) #Type theory #cs.ET #cs.LO #cs.PL #quant-ph
paper · pdf · doi:10.4204/eptcs.340.15
published as EPTCS 340, 2021, pp. 291-302 · In Proceedings QPL 2020, arXiv:2109.01534. See expanded version at arXiv:2012.02154
arxiv created 2021/09/06 · openalex publication_date 2021/09/06 · arxiv updated 2021/09/10 · openalex created_date 2021/09/13 · openalex updated_date 2026/08/06
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.