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

Coinduction is a widely used technique for establishing behavioural equivalence of programs in higher-order languages. In recent years, the rise of languages with quantitative (e.g. probabilistic) features has led to extensions of coinductive methods to more refined types of behavioural conformances, most notably notions of behavioural distance. To guarantee soundness of coinductive reasoning, one needs to show that the behavioural conformance at hand forms a program congruence, i.e. it is suitably compatible with the operations of the language. This is usually achieved by a complex proof technique known as Howe’s method, which needs to be carefully adapted to both the specific language and the targeted notion of behavioural conformance. We develop a uniform categorical approach to Howe’s method that features two orthogonal dimensions of abstraction: (1) the underlying higher-order language is modelled by an abstract higher-order specification (AHOS), a novel and very general categorical account of operational semantics, and (2) notions of behavioural conformance (such as relations or metrics) are modelled via fibrations over the base category of an AHOS. Our main result is a fundamental congruence theorem at this level of generality: Under natural conditions on the categorical ingredients and the operational rules of a language modelled by an AHOS, the greatest behavioural (bi)conformance on its operational model forms a congruence. We illustrate our theory by deriving congruence of bisimilarity and behavioural pseudometrics for probabilistic higher-order languages.

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