@article {3496, title = {The Quantum Abstract Machine}, year = {2024}, month = {2/21/2024}, abstract = {

This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The work is motivated by the need for conceptual tools for the development of quantum-communication systems that are usable by non-specialists in quantum physics while also correctly capturing at a useful abstraction the underlying quantum phenomena. Our approach involves defining a quantum abstract machine (QAM) whose operations correspond to well-known quantum circuits; these operations, however, are given direct abstract semantics in a style similar to that of Berry\&$\#$39;s and Boudol\&$\#$39;s Chemical Abstract Machine. This paper defines the QAM\&$\#$39;s semantics and shows via examples how it may be used to model and reason about existing quantum communication protocols.

}, url = {https://arxiv.org/abs/2402.13469}, author = {Liyi Li and Le Chang and Rance Cleaveland and Mingwei Zhu and Xiaodi Wu} } @article {3314, title = {Qafny: Quantum Program Verification Through Type-guided Classical Separation Logic}, year = {2023}, month = {7/12/2023}, abstract = {

Formal verification has been proven instrumental to ensure that quantum programs implement their specifications but often requires a significant investment of time and labor. To address this challenge, we present Qafny, an automated proof system designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. By modeling these operations as proof rules within a classical separation logic framework, Qafny provides automated support for the reasoning process that would otherwise be tedious and time-consuming. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs both into the Dafny programming language and into executable quantum circuits. Using Qafny, we demonstrate how to efficiently verify prominent quantum algorithms, including quantum-walk algorithms, Grover\&$\#$39;s search algorithm, and Shor\&$\#$39;s factoring algorithm, with significantly reduced human efforts.

}, url = {https://arxiv.org/abs/2211.06411}, author = {Liyi Li and Mingwei Zhu and Rance Cleaveland and Yi Lee and Le Chang and Xiaodi Wu} } @conference {2941, title = {Expanding the VOQC Toolkit}, booktitle = {The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021)}, year = {2021}, month = {06/2021}, abstract = {

voqc [Hietala et al. 2021b] (pronounced \“vox\”) is a compiler for quantum circuits, in the style of
tools like Qiskit [Aleksandrowicz et al. 2019], tket [Cambridge Quantum Computing Ltd 2019],
Quilc [Rigetti Computing 2019], and Cirq [Developers 2021]. What makes voqc different from these
tools is that it has been formally verified in the Coq proof assistant [Coq Development Team 2019].
voqc source programs are expressed in sqir, a simple quantum intermediate representation, which
has a precise mathematical semantics. We use Gallina, Coq\’s programming language, to implement
voqc transformations over sqir programs, and use Coq to prove the source program\’s semantics
are preserved. We then extract these Gallina definitions to OCaml, and compile the OCaml code to
a library that can operate on standard-formatted circuits.
voqc, and sqir, were built to be general-purpose. For example, while we originally designed sqir
for use in verified optimizations, we subsequently found sqir could also be suitable for writing, and
proving correct, source programs [Hietala et al. 2021a]. We have continued to develop the voqc
codebase to expand its reach and utility.
In this abstract, we present new extensions to voqc as an illustration of its flexibility. These
include support for calling voqc transformations from Python, added support for new gate sets
and optimizations, and the extension of our notion of correctness to include mapping-preservation,
which allows us to apply optimizations after mapping, reducing the cost introduced by making a
program conform to hardware constraints.

}, url = {http://rand.cs.uchicago.edu/files/planqc_2021c.pdf}, author = {Kesha Hietala and Liyi Li and Akshaj Gaur and Aaron Green and Robert Rand and Xiaodi Wu and Michael Hicks} } @article {2729, title = {Proving Quantum Programs Correct}, journal = {Schloss Dagstuhl}, year = {2021}, month = {7/13/2021}, abstract = {

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\&$\#$39;s algorithm, Grover\&$\#$39;s algorithm, and quantum phase estimation, a key component of Shor\&$\#$39;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.

}, doi = {https://doi.org/10.4230/LIPIcs.ITP.2021.21}, url = {https://arxiv.org/abs/2010.01240}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Liyi Li and Michael Hicks} } @article {2912, title = {Verified Compilation of Quantum Oracles}, year = {2021}, month = {12/13/2021}, abstract = {

Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum algorithm. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits among three different bases via the Quantum Fourier Transform and Hadamard operations, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM\&$\#$39;s design enabled us to prove correct VQO\&$\#$39;s compilers -- from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language -- and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement oracles used in Shor\&$\#$39;s and Grover\&$\#$39;s algorithms, as well as several common arithmetic operators. VQO\&$\#$39;s oracles have performance comparable to those produced by Quipper, a state-of-the-art but unverified quantum programming platform.

}, url = {https://arxiv.org/abs/2112.06700}, author = {Liyi Li and Finnegan Voichick and Kesha Hietala and Yuxiang Peng and Xiaodi Wu and Michael Hicks} }