log in  |  register  |  feedback?  |  help  |  web accessibility
PhD Defense: A Verified Software Toolchain for Quantum Programming
Kesha Hietala
Monday, May 16, 2022, 10:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Quantum computing is steadily moving from theory into practice, with small-scale quantum computers available for public use. Now quantum programmers are faced with a classical problem: How can they be sure that their code does what they intend it to do? I aim to show that techniques for classical program verification can be adapted to the quantum setting, allowing for the development of high-assurance quantum software, without sacrificing performance or programmability. In support of this thesis, I present several results in the application of formal methods to the domain of quantum programming, aiming to provide a high-assurance software toolchain for quantum programming. I begin by presenting SQIR, a small quantum intermediate representation deeply embedded in the Coq proof assistant, which has been used to implement and prove correct quantum algorithms such as Grover’s search and Shor’s factorization algorithm. Next, I present VOQC, a verified optimizer for quantum circuits that contains state-of-the-art SQIR program optimizations with performance on par with unverified tools. I additionally discuss VQO, a framework for specifying and verifying oracle programs, which can then be optimized with VOQC. Finally, I present developing work on providing assurance for a high-level industry quantum programming language, Q#, in the F* proof assistant.

Examining Committee:
Dean's Representative:
Dr. Michael Hicks    
Dr. Lawrence Washington    
Dr. Andrew Childs   
Dr. Leonidas Lampropoulos    
Dr. Robert Rand (Univ. of Chicago)
Dr. Xiaodi Wu     

Kesha Hietala is a CS PhD candidate at the University of Maryland, College Park, advised by Mike Hicks. She is interested broadly in program analysis and verification, with a focus on verifying compilers for quantum programs. She received her Bachelor's degree from the University of Minnesota, Twin Cities, and will be joining Amazon AWS this summer.

This talk is organized by Tom Hurst