Wed 17 Jun 2026 11:20 - 11:40 at Flatirons 4 - Quantum Computing Chair(s): Sara Achour

Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient – even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local – involving just a small number of qubits – making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation – a core subroutine in Shor's factoring algorithm.

Wed 17 Jun

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

11:00 - 12:40
Quantum ComputingPLDI Research Papers at Flatirons 4
Chair(s): Sara Achour Stanford University
11:00
20m
Talk
Verification of Recursively Defined Quantum CircuitsDistinguished Paper
PLDI Research Papers
Mingsheng Ying University of Technology Sydney, Zhicheng Zhang University of Technology Sydney
DOI
11:20
20m
Talk
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
PLDI Research Papers
Nengkun Yu Stony Brook University, Jens Palsberg University of California at Los Angeles, Thomas Reps University of Wisconsin-Madison
DOI
11:40
20m
Talk
Hybrid Path-Sums for Hybrid Quantum Programs
PLDI Research Papers
Christopĥe Chareton CEA List - Université Paris-Saclay, Sébastien Bardin CEA List - Université Paris-Saclay, Jad Issa CEA List - Université Paris-Saclay, Mathieu Nguyen CEA List - Université Paris-Saclay, Nicolas Blanco CEA List - Université Paris-Saclay
DOI
12:00
20m
Talk
[TOPLAS] VyZX: Formal Verification of a Graphical Quantum Language
PLDI Research Papers
Adrian Lehmann University of Chicago, Ben Caldwell University of Chicago, A: Bhakti Shah , William Spencer , Robert Rand University of Chicago
12:20
20m
Talk
Cobble: Compiling Block Encodings for Quantum Computational Linear AlgebraDistinguished Paper
PLDI Research Papers
Charles Yuan University of Wisconsin-Madison
DOI