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

This paper studies the design of programming languages with handlers of higher-order effectful operations – effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core calculus with higher-kinded impredicative polymorphism, handlers of higher-order effectful operations, and optionally general recursion. The distinctive design choice of this calculus is that handlers are carried by lawless raw monads, while the computation judgements still satisfy the monadic laws judgementally. We present the calculus with a logical framework and give denotational models of the calculus using realizability semantics. We prove closed-term canonicity and parametricity for the recursion-free fragment of the language using synthetic Tait computability and a novel form of the $\top\top$-lifting technique.

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