POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 15:15 - 15:40 at Dortoirs - Category Theory Chair(s): Kenji Maillard

In many situations one encounters an entity that resembles a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this entity is, in fact, a monoid in a suitable sense.

Category theorists have answered this question by providing a notion of monoid in a monoidal category, or more generally in a multicategory. While these encompass many examples, there remain cases which do not fit into these frameworks, such as the notion of relative monad and the modelling of call-by-push-value sequencing. In each of these examples, the leftmost and/or the rightmost factor of a multiplication or associativity law seems to be distinguished.

To include such examples, we generalize the multicategorical framework in two stages.

Firstly, we move to the framework of a left-skew multicategory (due to Bourke and Lack), which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished, such as the notion of relative monad.

Secondly, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost factor are distinguished, such as the notion of a category on a span, and the modelling of call-by-push-value sequencing.

In the bi-skew framework (which is the most general), we give a coherence result saying that a monoid corresponds to an unbiased monoid, i.e. a map from the terminal bi-skew multicategory.

Thu 15 Jan

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

14:00 - 15:40
Category TheoryPOPL at Dortoirs
Chair(s): Kenji Maillard Inria
14:00
25m
Talk
Classical Notions of Computation and the Hasegawa-Thielecke Theorem
POPL
Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA
DOI
14:25
25m
Talk
From Semantics to Syntax: A Type Theory for Comprehension Categories
POPL
Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University
DOI
14:50
25m
Talk
Higher-Order Behavioural Conformances via Fibrations
POPL
Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg
DOI
15:15
25m
Talk
What Is a Monoid?
POPL
Paul Blain Levy University of Birmingham, Morgan Rogers University Sorbonne Paris 13
DOI