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

Relative monads provide a controlled view of computation. We generalise the monadic metalanguage to a relative setting and give a complete semantics with strong relative monads. Adopting this perspective, we generalise two existing program calculi from the literature. We provide a linear-non-linear language for graded monads, LNL-RMM, along with a semantic proof that it is a conservative extension of the graded monadic metalanguage. Additionally, we provide a complete semantics for the arrow calculus, showing it is a restricted relative monadic metalanguage. By lifting these restrictions, we introduce ARMM, a computational lambda calculus-style language for arrows that conservatively extends the arrow calculus.

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