POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Fri 16 Jan 2026 14:00 - 14:25 at Dortoirs - Monads and Effects Chair(s): Henning Urbat

We use the theory of algebraic effects to give a complete equational axiomatization for dynamic threads.
Our method is based on parameterized algebraic theories, which give a concrete syntax for strong monads on functor categories, and are a convenient framework for names and binding.

Our programs are built from the key primitives fork' andwait'. Fork' creates a child thread and passes its name (thread ID) to the parent thread.Wait' allows us to wait for given child threads to finish.
We provide a parameterized algebraic theory built from fork and wait, together with basic atomic actions and laws such as associativity of `fork'.

Our equational axiomatization is complete in two senses.
First, for closed expressions, it completely captures equality of labelled posets (pomsets), an established model of concurrency: model complete. Second, any two open expressions are provably equal if they are equal under all closing substitutions: syntactically complete.

The benefit of algebraic effects is that the semantic analysis can focus on the algebraic operations of fork and wait.
We then extend the analysis to a simple concurrent programming language by giving operational and denotational semantics.
The denotational semantics is built using the methods of parameterized algebraic theories and we show that it is sound, adequate, and fully abstract at first order for labelled-poset observations.

Fri 16 Jan

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

14:00 - 15:40
Monads and EffectsPOPL at Dortoirs
Chair(s): Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg
14:00
25m
Talk
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper
POPL
Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford
DOI
14:25
25m
Talk
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
POPL
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
DOI
14:50
25m
Talk
Rows and Capabilities as Modal Effects
POPL
Wenhao Tang The University of Edinburgh, Sam Lindley University of Edinburgh
DOI
15:15
25m
Talk
The Relative Monadic Metalanguage
POPL
Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford
DOI