Programme
The schedule consists of regular talks, short contributions, and invited talks. See also the ETAPS Satellite Events programme.
Days: | Saturday (Apr 11) | Sunday (Apr 12) |
Saturday, April 11, 2026
|
9:00
- | 10:00 |
Invited Talk:
Bialgebraic Methods for Programming Languages
Abstract The semantics of programming languages has traditionally developed along two complementary lines: denotational and operational. Denotational semantics is intrinsically mathematical, with category theory providing a natural and well-developed foundation that has been cultivated over decades. Operational semantics, in contrast, is inherently syntactic and intensional, lacks a uniform notion of rule format, and has therefore proved more resistant to systematic categorical treatment.
Building on the seminal bialgebraic approach to operational semantics by Turi and Plotkin, this talk presents a programme of Higher-Order Mathematical Operational Semantics. The aim is to leverage bialgebraic techniques to the setting of programming languages, yielding a structural and compositional account of operational semantics that supports robust reasoning on programs.
The pivotal step in this programme is the identification of the notion of abstract higher-order GSOS law, together with a corresponding compositionality theorem, generalising Turi and Plotkin's first-order setting and opening the way to higher-order programming languages. This talk presents the core framework and highlights two selected directions. First, it shows how (higher-order) lax bialgebras provide an abstract setting for weak applicative bisimilarity. Second, it outlines an abstract account of operational logical relations for languages specified by higher-order GSOS laws.
|
|
10:00
- | 10:30 |
Coffee Break
|
|
10:30
- | 11:10 |
Learning Automata with Name Allocation
Abstract Automata over infinite alphabets have emerged as a convenient computational model for processing structures involving data, such as nonces in cryptographic protocols or data values in XML documents. They are naturally modelled as coalgebras for suitable type functors on the category of nominal sets.
We introduce active learning methods for bar automata, a species of automata that process finite data words represented as bar strings, which are words with explicit name binding letters. Bar automata have pleasant algorithmic properties. We develop a framework in which every learning algorithm for standard deterministic or non-deterministic finite automata over finite alphabets can be used to learn bar automata, with a query complexity determined by that of the chosen learner. The technical key to our approach is the algorithmic handling of $\alpha$-equivalence of bar strings, which allows to bridge the gap between finite and infinite alphabets. The principles underlying our framework are generic and also apply to bar Büchi automata and bar tree automata, leading to the first active learning methods for data languages of infinite words and finite trees. |
|
11:10
- | 11:50 |
A Framework for Coalgebraic Reward-Sensitive Bisimulation
Abstract In this paper we present a framework for modelling reward-sensitive bisimulations, that is, bisimulations that account for quantitative differences such as accumulated rewards. To capture both qualitative and quantitative aspects uniformly, we consider two interacting notions of bisimulation: a graded variant that tracks bounded reward differences, and an ungraded one that abstracts from them.
Our characterization of these notions is done in the fibrational and coalgebraic approaches initiated by Hermida and Jacobs. To formally relate the graded and ungraded notions, we deploy categorical gluing, a standard technique in categorical logic. Furthermore, we show that this construction interacts well with standard coalgebra concepts, such as final coalgebras, and that it yields a unified characterization in terms of combined notions of bisimulations under mild assumptions.
In order to demonstrate the versatility of our approach, we show how it encompasses various bisimulation notions for different kinds of systems, including relation-based bisimulations for automata with rewards and metric-based notions of bisimulations for labelled Markov processes.
|
|
11:50
- | 12:30 |
The Only Distributive Law Over the Powerset Monad Is the One You Know
Abstract Distributive laws of set functors over the powerset monad (also known as Kleisli laws for the powerset monad) are well-known to be in one-to-one correspondence with extensions of set functors to functors on the category of sets and relations. We study the question of existence and uniqueness of such distributive laws. Our main result entails that an accessible set functor admits a distributive law over the powerset monad if and only if it preserves weak pullbacks, in which case the so-called power law (which induces the Barr extension) is the unique one. Furthermore, we show that the powerset functor admits exactly three distributive laws over the powerset monad, revealing that uniqueness may fail for non-accessible functors. |
|
12:30
- | 14:00 |
Lunch Break
|
|
14:00
- | 15:00 |
Invited Talk:
The Hennessy–Milner Theorem as a Shadow of Determinacy in the Bisimulation Game (Tutorial)
Abstract The Hennessy–Milner theorem is one of the classic results in concurrency
theory: Two states in a transition system can be related by a bisimulation
precisely if they cannot be told apart by any modal-logic formula.
In this tutorial, we revisit this duality from the perspective of equivalence
games: An attacker tries to point out differences and a defender attempts to
parry the challenges. Interestingly, the Hennessy–Milner theorem turns out to
just be a *shadow* of the determinacy in such games.
We survey how the game perspective helps with proofs, intuitions, tools, and
systematization.
|
|
15:00
- | 15:20 |
Locally Final Coalgebras in Denotational Semantics
Abstract The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching. |
|
15:20
- | 15:40 |
Sheaves on categories of coalgebras
Abstract We define Grothendieck topologies on categories whose objects are coalgebras---specifically, Mealy machines over definable sets in an o-minimal structure---rather than on base categories of time or observations.
We prove that coalgebra categories inherit adhesivity from the base (under a pullback-preservation condition on the functor), construct a site of definable open immersions, and show that behavioural equivalence yields a separated presheaf of explanations.
The framework is motivated by interpretability in machine learning. |
|
15:40
- | 16:00 |
Intrinsically Correct Algorithms and Recursive Coalgebras
Abstract Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, thecorrectness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defi ned recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense
that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda. |
|
16:00
- | 16:30 |
Coffee Break
|
| 19:30 |
Workshop Dinner
Abstract The dinner takes place in the restaurant on the square where also the coffee
and lunch breaks are.
Tables are labelled with workshop names, but we were told that you are free
to roam.
The menu can be found here: https://bit.ly/m/etaps-menu.
Please inform the staff if you have dietary restrictions when you arrive.
The bar opens at 17:30 if you plan to stay around until the dinner starts.
|
Sunday, April 12, 2026
|
9:00
- | 10:00 |
Invited Talk:
Behavioural Metrics, Congruences and Up-To Techniques
Abstract Behavioural equivalences such as bisimilarity and trace equivalence specify
whether two system states exhibit the same behaviour or deviating behaviour.
It is sometimes desirable to consider a quantitative instead of a qualitative
notion of behavioural equivalence, a so-called behavioural metric.
Such metrics measure the behavioural distance of two states, allowing
statements such as "the behaviour of two states differs only by epsilon".
The aim of this talk is to give a uniform account of bisimilarity metrics in a
coalgebraic setting.
As instances, I will discuss metric transition systems by de Alfaro, Faella
and Stoelinga and pseudometrics for probabilistic transition systems by van
Breugel and Worrell.
The latter approach has close connections to a duality from transportation
theory, also known as Kantorovich-Rubinstein duality.
Furthermore I will explain how compact witnesses for upper bounds of
behavioural distances can be obtained via up-to techniques and the relation to
metric congruences.
|
|
10:00
- | 10:30 |
Coffee Break
|
|
10:30
- | 11:10 |
Coalgebraic Semantics for Two-agent ATL and its Meta-level Model-checking Complexity
Abstract We reformulate the semantics for Alternating-time Temporal Logic (ATL) by extending the classical notion of strategy with Kleisli maps. We introduce a meta-level, coalgebraic semantics for ATL parametrized by Kleisli maps of a monad known as the serial monotone neighborhood monad. Especially, we focus on such Kleisli maps, called forward/backward (fwd/bwd) execution maps, that are defined as post/pre-fixpoints of the coalgebraic infinitary trace operator of the monad, respectively. This extension not only provides a categorically neat meta-theory of ATL unifying existing semantics for ATL, including classical history-dependent and fair ones and also history-free one, but also enables meta-level analysis of ATL's model-checking efficiency. Our main technical results are the following two. First, we clarify the rigorous correspondence between classes of strategies and our fwd or bwd execution maps, by identifying the exact properties which make a class of strategies into a fwd/bwd execution map. With these properties, we observe that the existing semantics for ATL mentioned above naturally become instances of our coalgebraic semantics. Second, we analyze the model-checking efficiency of ATL under the coalgebraic semantics via a fixpoint encoding into the mu-calculus. We formulate a meta-level model-checking algorithm with linear-time complexity using this encoding, which approximates liveness and safety formulas written in ATL, and even returns the exact interpretations when some additional conditions are satisfied. |
|
11:10
- | 11:50 |
Coalgebraic Semantics for Fischer Servi Intuitionistic Modal Logic
Abstract We present a new coalgebraic semantics for the intuitionistic modal logic known as IK or Fischer Servi logic. Only recently, a construction introduced by Almeida has made coalgebraic analysis of intuitionistic modal logics possible. In particular, it provides a functorial method of turning coalgebras for a positive modal logic into coalgebras for its least intuitionistic extension. This does not suffice on its own to treat Fischer Servi logic, as it is not the least intuitionistic extension of a positive modal logic. Thus, we fill this gap in the research by providing a modified approach, which yields coalgebraic completeness for IK and other related logics. As an application of these results, we study bisimulations for Fischer Servi logic, describe the dual spaces of free IK algebras, and show how our approach can be used to capture rank-1 extensions of IK. |
|
11:50
- | 12:30 |
Coalgebraic Path Constraints
Abstract Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques come from coalgebraic modal logic, pattern avoidance specifications, and hidden algebra. We introduce equational path constraints, a well-behaved and relatively easy to describe class of finitary behavioural properties that provide an algebra-flavoured alternative to coequations. The basic idea is to assign a pair of values to each path through a coalgebra and posit that the two values coincide. We show that equational path constraints define covarieties and construct final coalgebras relative to equational path constraints in some concrete cases. We connect equational path constraints to coequations when values computed from paths live in a monad, and we compute an upper bound on the number of colours needed to express the coequation. One of our constructions is reminiscent of the initial/terminal sequences of (Adámek, 1974) and (Barr, 1993). Motivating examples include commutativity conditions in automata theory, differential equations, bi-infinite streams, and frame conditions. |
|
12:30
- | 14:00 |
Lunch Break
|
|
14:00
- | 14:40 |
On Axioms of Arboreal Categories
Abstract Arboreal categories were introduced as an axiomatic framework for game comonads, which provide a comonadic view on many model-comparison games in logic. In this note, we point out an inadequacy of one of the axioms of arboreal categories stating that paths are connected. We then propose a new notion of tree-connectedness to address this deficiency. Moreover, we show that with this new definition all essential properties of arboreal categories that we are aware of remain valid and, furthermore, that the path functor is a Street fibration.
|
|
14:40
- | 15:00 |
Break
|
|
15:00
- | 15:20 |
Many-valued Coalgebraic Lindstrom’s Theorem
Abstract Inspired by the works on Lindstrom's theorem of modal logic done by M. de Rijke and van Benthem, A. Kurz and Y. Venema proved three Lindstrom's theorems characterizing coalgebraic logic. They proposed an abstract coalgebraic logic and proved that any coalgebraic logic extend from the abstract logic satisfying invariance under bisimulation, Boolean closeness, compactness, and expressively closed at $\omega$ is equivalent to . Nevertheless, their work is based on final-coalgebra approximation instead of submodels. S. Enquvist improved the results through proposing the definition of submodels in coalgebraic logic. Since many-valued coalgebraic modal logic has been widely studied , it is natural to investigate which logical properties characterize a many-valued coalgebraic modal logic. In this talk, we will prove a many-valued coalgebraic Lindstrom theorem. |
|
15:20
- | 15:40 |
Infinite Strategies in Two-Player Games
Abstract The coalgebraic study of infinite linear-time semantics was initiated
by Jacobs, where it was shown that linear-time semantics in
labelled transition systems cannot be captured be finality in a Kleisli
category, but instead by the greatest coalgebra morphism.
This contribution describes some recent work by Plummer and Cirstea,
about infinite linear-time semantics in the richer structure
of a two-player game: a transition system with two flavours of non-determinism.
The semantics at a state in the game is
described by the set of strategies starting from that state;
we find that the infinite trace map, assigning states to semantics,
can be computed as a greatest, and least, fixed point. |
|
15:40
- | 16:00 |
Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
Abstract We present a theory of behavioural distances, quantitative (bi)simulations and
expressive modal logics which are all expressed in terms of mixed-type predicate
liftings for a functor F that lift binary predicates on a set X into real-valued
predicates on the set FX. The quintessential example of such a lifting is the
probability lifting for the distribution functor, which evaluates probability
measures on subsets and for which the resulting behavioural distance relates to
the Lévy-Prokhorov metric and ε-simulations. We show that behavioural distances
in our framework admit multiple equivalent representations, via simulations, via
a spoiler-duplicator game and via both two-valued and real-valued coalgebraic
modal logics; for the latter two, we present algorithms to extract formulae that
witness distances between states. |
| 16:00 |
Coffee Break & Closing
|