POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Mon 12 Jan 2026 12:05 - 12:25 at Salle 14 - Session 2

We describe a categorical model of MALL (Multiplicative Additive Linear Logic) inspired by the Heisenberg-Schrödinger duality of finite-dimensional quantum theory. Proofs of formulas with positive logical polarity correspond to CPTP (completely positive trace-preserving) maps in our model, i.e. the quantum operations in the Schrödinger picture, whereas proofs of formulas with negative logical polarity correspond to CPU (completely positive unital) maps, i.e. the quantum operations in the Heisenberg picture. The mathematical development is based on noncommutative geometry and finite-dimensional von Neumann (co)algebras, which can be defined as special kinds of (co)monoid objects internal to the category of finite-dimensional operator spaces.

Extended Abstract (qcs.pdf)1.47MiB

Mon 12 Jan

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

11:00 - 12:30
Session 2PLanQC at Salle 14
11:00
45m
Keynote
Democratizing quantum formal verification: the path-sum wayKeynote
PLanQC
Christopĥe Chareton CEA, LIST, France
11:45
20m
Talk
One rig to control them allTalk
PLanQC
Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Louis Lemonnier University of Edinburgh
File Attached
12:05
20m
Talk
Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic ApproachTalk
PLanQC
Thea Li Inria, LMF, ENS Paris-Saclay, Université Paris-Saclay, Vladimir Zamdzhiev Inria
File Attached