POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Mon 12 Jan 2026 15:10 - 15:30 at Salle 14 - Session 3

To make quantum computing more practical and ubiquitous, we must develop more general and robust ways to detect bugs in quantum programs. Prior work on runtime quantum assertions has focused on the expressiveness of individual assertions and their construction as quantum circuits, but a complementary question—how to effectively check multiple assertions in a quantum program—has been less explored.

In this work, we study the time–space trade-offs for testing quantum assertions in a practical hardware setting without mid-circuit measurement. We formalize this setting and analyze the FirstFail problem—outputting the first failing assertion among n program assertions. We give a single-run strategy that uses O(log n) ancilla qubits, and we prove a matching lower bound showing that any strategy must satisfy T × S = Ω(log n), where T is the number of runs and S is the number of ancilla qubits used per run.

This asymptotically improves over the O(n) product achieved by two naïve baselines (i.e., using a single run with n ancillae, or using a single ancilla with n runs). Moreover, it also shows that mid-circuit measurement does not yield a decisive advantage: it yields only O(log n) advantage, not O(n), over strategies not relying on mid-circuit measurements.

Extended Abstract (planqc26-paper6.pdf)832KiB

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

13:50 - 15:30
Session 3PLanQC at Salle 14
13:50
20m
Talk
A Graded Modal Type Theory for Pulse SchedulesTalk
PLanQC
Robin Adams Chalmers University of Technology, Gothenburg University, Sweden, Jean-Philippe Bernardy Chalmers University of Technology, Gothenburg University, Sweden, Lorenzo Perticone Chalmers University of Technology, Gothenburg University, Sweden, Jeremy Pope Chalmers University of Technology, Gothenburg University, Sweden
File Attached
14:10
20m
Talk
Efficient Parallel Compilation and Profiling of Quantum Circuits at Large ScalesTalk
PLanQC
Jane Moore Queen's University Belfast, Michael Hart Queen's University Belfast, John McAllister Queen's University Belfast
File Attached
14:30
20m
Talk
A Unified Assertion-Based Framework for Classical-Quantum Program VerificationTalk
PLanQC
File Attached
14:50
20m
Talk
A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilation and EmulationRemote
PLanQC
Yu-Hsuan Wu Academia Sinica, Yue Shi Princeton University, Junyi Liu University of Maryland, Yuxiang Peng Purdue University
File Attached
15:10
20m
Talk
Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies and Lower BoundsRemote
PLanQC
Shengyuan Yang University of Wisconsin-Madison, Charles Yuan University of Wisconsin–Madison
File Attached