01160nas a2200157 4500008004100000245003700041210003700078260001400115520074900129100001900878700001700897700001900914700001300933700001900946856003700965 2021 eng d00aProving Quantum Programs Correct0 aProving Quantum Programs Correct c7/13/20213 a
As quantum computing steadily progresses from theory to practice, programmers are faced with 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 Simon's algorithm, 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.
1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aLi, Liyi1 aHicks, Michael uhttps://arxiv.org/abs/2010.01240