Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed.
To this end, we introduce a simple syntax for generating unitaries from "just a phase"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the "if let" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design.
We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:10 - 17:25 | |||
16:10 25mTalk | Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI | ||
16:35 25mTalk | On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI | ||
17:00 25mTalk | Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI | ||