Software Assurance for Quantum Programs
Abstract
Quantum programming is hard. Programs are hard to write, hard to test and hard to debug- quantum superposition and entanglement are unintuitive and surprising, as is the destructive nature of quantum measurement. We aim to address these problems using techniques from the areas of programming languages and formal, mathematical verification. We propose to take the VOQC compiler we previously developed and expand it to a Verified Quantum Computing Stack, that supports a variety of programming languages and approaches to proving programs correct. We will incorporate high-level languages within the stack, allowing us to write more intuitive programs but still be able to prove properties of those programs and execute them. We will augment these languages with powerful type checking systems that will guide program development and catch common classes of errors. Finally, we will develop tools to help reason about noisy quantum program executions, and to identify and diagnose program bugs.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 07, 2023
- Source ID
- FA95502110051
Entities
People
- Michael Hicks
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Maryland