POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This program is tentative and subject to change.

Wed 14 Jan 2026 15:15 - 15:40 at Dortoirs - Quantum 1 Chair(s): Ugo Dal Lago

Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies.

This program is tentative and subject to change.

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
Hide past events