Quantum computing is steadily moving from theory into practice, with small-scale quantum computers available for public use. Now programmers are faced with the standard problem: How can they be sure that their code does what they intend it to do? This dissertation proposal presents encouraging results in the application of formal methods to the domain of quantum programming. Using the Coq proof assistant we have mechanized proofs of several textbook quantum algorithms including the Deutsch-Jozsa algorithm, Simon's algorithm, and quantum phase estimation. We have also implemented several state-of-the-art quantum program optimizations and mathematically proved them to be semantics-preserving. In this proposal I will discuss work on our small quantum intermediate representation (SQIR) and verified optimizer for quantum circuits (VOQC). I will also present plans for extending our verified software toolchain to include high-level quantum languages.

Examining Committee: 

 

                          Chair:               Dr. Michael Hicks
                          Dept rep:         Dr. Leonidas Lampropoulos
                          Members:        Dr. Xiaodi Wu    
                                                    Dr.  Andrew Childs
                                                    Dr. Robert Rand