POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 14:00 - 14:25 at Dortoirs - Quantum 1 Chair(s): Ugo Dal Lago

In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques such as Gödelization to prove that this language is expressive with respect to the quantum programs with loops—specifically, for any program $S$ and any postcondition $\psi$ formulated in the assertion language, the weakest precondition of $S$ with respect to $\psi$ can also be expressed as a formula in the assertion language. As an application, we present a sound and relatively complete quantum Hoare logic upon our expressive assertion language.

Wed 14 Jan

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

14:00 - 15:40
Quantum 1POPL at Dortoirs
Chair(s): Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur
14:00
25m
Talk
An Expressive Assertion Language for Quantum Programs
POPL
Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences
DOI
14:25
25m
Talk
Hadamard-Pi: Equational Quantum Programming
POPL
Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark
DOI
14:50
25m
Talk
Qudit Quantum Programming with Projective Cliffords
POPL
Jennifer Paykin University of Vermont, Sam Winnick Simon Fraser University; University of Waterloo
DOI
15:15
25m
Talk
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
POPL
Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz
DOI Pre-print