Hoare Types for Quantum Programming Languages


Quantum Computing is a new and upcoming way to utilize Quantum Mechanics for computation. It is easy to introduce bugs while programming quantum computers similar to classical computing. Strong static type systems have prevented a lot of bugs from being introduced in the classical paradigm. There is a similar need for well-designed types in the domain of quantum computing. We introduce Quantum Hoare Types that let programmers reason statically about certain semantic properties of their quantum programs and further allow a limited form of formal verification.

ACM Student Research Competition at Principles of Programming Languages (POPL) 2020

Extended abstract accepted for the poster session of POPL 2020 SRC.

Feedback on this poster from the POPL community led to Quantum Hoare Type Theory (QHTT) that was accepted at QPL 2020.