Wed 23 Oct 2024 15:00 - 15:20 at IBR East - Static Analysis and Program Verification 2 Chair(s): Anders Møller

Quantum algorithms for tasks such as factorization, search, and simulation rely on control flow such as branching and iteration that depends on the value of data in superposition. High-level programming abstractions for control flow, such as switches, loops, higher-order functions, and continuations, are ubiquitous in classical languages. By contrast, many quantum languages do not provide high-level abstractions for control flow in superposition, and instead require the use of hardware-level logic gates to implement such control flow.

The reason for this gap is that whereas a classical computer supports control flow abstractions using a program counter that can depend on data, the typical architecture of a quantum computer does not analogously provide a program counter that can depend on data in superposition. As a result, the complete set of control flow abstractions that can be correctly realized on a quantum computer has not yet been established.

In this work, we provide a complete characterization of the properties of control flow abstractions that are correctly realizable on a quantum computer. First, we prove that even on a quantum computer whose program counter exists in superposition, one cannot correctly realize control flow in quantum algorithms by lifting the classical conditional jump instruction to work in superposition. This theorem denies the ability to directly lift general abstractions for control flow such as the λ-calculus from classical to quantum programming.

In response, we present the necessary and sufficient conditions for control flow to be correctly realizable on a quantum computer. We introduce the quantum control machine, an instruction set architecture featuring a conditional jump that is restricted to satisfy these conditions. We show how this design enables a developer to correctly express control flow in quantum algorithms using a program counter in place of logic gates.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Static Analysis and Program Verification 2OOPSLA 2024 at IBR East
Chair(s): Anders Møller Aarhus University
13:40
20m
Talk
HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing
OOPSLA 2024
Yiyu Zhang Nanjing University, Tianyi Liu Nanjing University, Yueyang Wang Nanjing University, Yun Qi Nanjing University, Kai Ji Nanjing University, Jian Tang Nanjing University, Xiaoliang Wang Nanjing University, Xuandong Li Nanjing University, Zhiqiang Zuo Nanjing University
DOI
14:00
20m
Talk
MEA2: a Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang
OOPSLA 2024
Boyao Ding University of Science and Technology of China, Qingwei Li University of Science and Technology of China, Yu Zhang University of Science and Technology of China, Fugen Tang University of Science and Technology of China, Jinbao Chen University of Science and Technology of China
DOI
14:20
20m
Talk
Newtonian Program Analysis of Probabilistic Programs
OOPSLA 2024
Di Wang Peking University, Thomas Reps University of Wisconsin-Madison
DOI
14:40
20m
Talk
Non-Termination Proving at Scale
OOPSLA 2024
Azalea Raad Imperial College London, Julien Vanegue Imperial College London; Bloomberg, Peter W. O'Hearn Lacework; University College London
DOI
15:00
20m
Talk
Quantum Control Machine: The Limits of Control Flow in Quantum Programming
OOPSLA 2024
Charles Yuan Massachusetts Institute of Technology, Agnes Villanyi MIT CSAIL, Michael Carbin Massachusetts Institute of Technology
DOI