%0 Journal Article %J 12th International Conference on Interactive Theorem Proving (ITP 2021) %D 2021 %T Proving Quantum Programs Correct %A Hietala, Kesha %A Rand, Robert %A Hung, Shih-Han %A Li, Liyi %A Hicks, Michael %E Cohen, Liron %E Kaliszyk, Cezary %X

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.

%B 12th International Conference on Interactive Theorem Proving (ITP 2021) %V 193 %P 21:1–21:19 %8 06/2021 %@ 978-3-95977-188-7 %G eng %U https://drops.dagstuhl.de/opus/volltexte/2021/13916 %R 10.4230/LIPIcs.ITP.2021.21 %0 Journal Article %J 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) %D 2021 %T Quantum Query Complexity with Matrix-Vector Products %A Andrew M. Childs %A Hung, Shih-Han %A Li, Tongyang %X

We study quantum algorithms that learn properties of a matrix using queries that return its action on an input vector. We show that for various problems, including computing the trace, determinant, or rank of a matrix or solving a linear system that it specifies, quantum computers do not provide an asymptotic speedup over classical computation. On the other hand, we show that for some problems, such as computing the parities of rows or columns or deciding if there are two identical rows or columns, quantum computers provide exponential speedup. We demonstrate this by showing equivalence between models that provide matrix-vector products, vector-matrix products, and vector-matrix-vector products, whereas the power of these models can vary significantly for classical computation.

%B 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) %I Schloss Dagstuhl – Leibniz-Zentrum für Informatik %C Dagstuhl, Germany %8 2/7/2021 %@ 978-3-95977-195-5 %G eng %U https://drops.dagstuhl.de/opus/volltexte/2021/14124 %R 10.4230/LIPIcs.ICALP.2021.55