Proving Quantum Programs Correct

TitleProving Quantum Programs Correct
Publication TypeJournal Article
Year of Publication2021
AuthorsHietala, K, Rand, R, Hung, S-H, Li, L, Hicks, M
Secondary AuthorsCohen, L, Kaliszyk, C
Journal12th International Conference on Interactive Theorem Proving (ITP 2021)
Date Published06/2021
ISBN Number978-3-95977-188-7

As quantum computing progresses steadily from theory into practice, programmers will face
a common problem: How can they be sure that their code does what they intend it to do? This
paper presents encouraging results in the application of mechanized proof to the domain of quantum
programming in the context of the sqir development. It verifies the correctness of a range of a
quantum algorithms including Grover’s algorithm and quantum phase estimation, a key component
of Shor’s algorithm. In doing so, it aims to highlight both the successes and challenges of formal
verification in the quantum context and motivate the theorem proving community to target quantum
computing as an application domain.