SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 14:30 - 15:00 at Lecture Theatre 2 - Quantum Chair(s): Jan Vitek

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 program. 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 between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM’s design enabled us to prove correct VQO’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 a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor’s and Grover’s algorithms. We found that VQO’s QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using “classical” gates; VQO’s versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
QuantumOOPSLA at Lecture Theatre 2
Chair(s): Jan Vitek Northeastern University
13:30
30m
Research paper
Bugs in Quantum computing platforms: an empirical study
OOPSLA
Matteo Paltenghi University of Stuttgart, Germany, Michael Pradel University of Stuttgart
DOI
14:00
30m
Talk
Tower: Data Structures in Quantum Superposition
OOPSLA
Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI
14:30
30m
Talk
Verified Compilation of Quantum Oracles
OOPSLA
Liyi Li University of Maryland, Finn Voichick University of Maryland, Kesha Hietala University of Maryland, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland, Michael Hicks University of Maryland; Amazon
DOI