POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 10:00 - 10:20 at Kelvin Lecture - Synthesis 2 Chair(s): Michael Hicks

Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of \emph{program synthesis} for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes ten quantum unitary programs including quantum adder circuits, quantum eigenvalue inversion circuits and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.

Thu 18 Jan

Displayed time zone: London change

09:00 - 10:20
Synthesis 2POPL at Kelvin Lecture
Chair(s): Michael Hicks Amazon Web Services and the University of Maryland
09:00
20m
Talk
Semantic Code Refactoring for Abstract Data Types
POPL
Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
09:20
20m
Talk
API-driven Program Synthesis for Testing Static Typing Implementations
POPL
Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich
09:40
20m
Talk
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
10:00
20m
Talk
A Case for Synthesis of Recursive Quantum Unitary Programs
POPL
Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland