Quantum Hoare Type Theory

Kartik Singhal, John Reppy
Mar 31, 2021

Toward a unified system for programming, specifying, and reasoning about quantum programs.

Formal Specification Formal Verification Hoare Logic Language Design Pre- and Postconditions Program Proof Program Specifications Programming Languages Quantum Computation Quantum Computing Separation Logic Type Systems Type Theory

Publications

Kartik Singhal (2020). Quantum Hoare Type Theory. UChicago CS: MS Paper.

PDF Cite Project Slides Video arXiv

Kartik Singhal, John Reppy (2020). Quantum Hoare Type Theory: Extended Abstract. QPL 2020.

PDF Cite Project Slides Video DOI Venue

Kartik Singhal (2019). Hoare Types for Quantum Programming Languages. POPL 2020 SRC.

PDF Cite Project Poster Venue