Formal methods of quantum program analysis

Quantum computation is rapidly moving out of science fiction and into reality. With these growing computational devices larger and more complex quantum algorithms are increasingly being programmed, compiled, and run on a wide range of hardware. Accordingly, quantum programming languages and compilers are becoming more intricate, bringing new challenges to the scalable design and verification of quantum programs. To address these challenges, as with classical computing we need a mature ecosystem of tools for the analysis of quantum programs. In this talk, I will discuss some formal methods for the analysis of quantum programs and show how they can be used to improve the reliability of quantum compilers as well as power up circuit optimizations.