2026-08-18T05:51:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13916 2024-03-06T10:53:07Z ddc:004 open_access

Proving Quantum Programs Correct Hietala, Kesha Rand, Robert Hung, Shih-Han Li, Liyi Hicks, Michael Formal Verification Quantum Computing Proof Engineering 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kesha Hietala and Robert Rand and Shih-Han Hung and Liyi Li and Michael Hicks 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.21 urn:nbn:de:0030-drops-139160 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.21 eng https://creativecommons.org/licenses/by/4.0/legalcode