Programme
The schedule consists of regular talks, short contributions, and invited talks.
Days:  Saturday (Apr 06)  Sunday (Apr 07) 
Saturday, April 06, 2024
8:50  9:00 
Opening

9:00  10:00 
Codensity Liftings and Their Applications (Keynote)
Slides
Abstract Codensity lifting is a method to construct liftings of endofunctors/monads along fibrations. They subsume several constructions in mathematics, such as the Kantorovich metric and the lower/upper preorder on powersets, and are applied to the semantics of programming languages and transition systems. In this talk, I will talk about 1) an overview of codensity lifting, 2) applications of codensity liftings to bisimulation games and program semantics, and 3) recent development of lifting distributive laws to codensitylifted functors. 
10:00  10:30 
Coffee Break

10:30  11:00 
Coalgebraic CTL: Fixpoint Characterization and PolynomialTime Model Checking
Preprint Slides
Abstract We introduce a pathbased coalgebraic temporal logic, Coalgebraic CTL (CCTL), as a categorical abstraction of standard Computation Tree Logic (CTL). Our logic can be used to formalize properties of systems modeled as coalgebras with branching. We present the syntax and pathbased semantics of CCTL, and show how to encode this logic into a coalgebraic fixpoint logic with a stepwise semantics. Our main result shows that this encoding is semanticspreserving. We also present a polynomialtime modelchecking algorithm for CCTL, inspired by the standard modelchecking algorithm for CTL but described in categorical terms. A key contribution of our paper is to identify the categorical essence of the standard encoding of CTL into the modal mucalculus. This categorical perspective also explains the absence of a similar encoding of PCTL (Probabilistic CTL) into the probabilistic mucalculus. 
11:00  11:30 
A Categorical Approach to Coalgebraic Fixpoint Logic
Preprint Slides
Abstract We define a framework for incorporating fixpoint logics into the dualadjunction setup for coalgebraic modal logics. We achieve this by using orderenriched categories. We give a leastsolution semantics as well as an initialalgebra semantics, and prove they are equivalent. We also show how to place the alternationfree coalgebraic mucalculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality. 
11:30  12:00 
PreorderConstrained Simulations for Program Refinement with Effects
Preprint Slides
Abstract We propose a notion of preorderconstrained simulation. It is parameterised by a preorder ("observation preorder") on traces, so that it can uniformly characterise quantitative notions of program refinement for different effects, such as exception, nondeterminism and I/O.
Preorderconstrained simulation is additionally parameterised by a positive number ("lookahead bound"), and forms a generative spectrum governed by the lookahead bound. We analyse the complexity of determining preorderconstrained similarity, and show that preorderconstrained simulation can be enhanced by the socalled upto technique. 
12:00  12:30 
Coinductive Reasoning about CRDT Emulation
Preprint Slides
Abstract Conflictfree replicated data types (CRDTs) are distributed data structures
designed for fault tolerance and high availability. CRDTs have historically been
taxonomized into operationbased (or opbased) CRDTs and statebased CRDTs. The
notion that statebased and opbased CRDTs are equivalent is often appealed to
in the literature. In particular, verification techniques and results for one
kind of CRDT are often said to be applicable to the other kind, thanks to this
equivalence. However, while there are general algorithms for constructing a
statebased CRDT from a given opbased CRDT and vice versa, what it means for
one kind of CRDT to emulate another has never been made fully precise. In this
paper, we model CRDT systems as transition system coalgebras, and argue that
emulation can be understood formally in terms of various weak simulations between the
coalgebras of the original and emulating CRDT systems. As
a simple corollary, we deduce which properties are preserved by the emulation
algorithms, thus closing a gap in the CRDT literature. 
12:30  14:00 
Lunch Break

14:00  15:00 
Learning OmegaRegular Languages  A Tour via Learning Paradigms and Canonical Representations (Invited Talk)
Abstract While regular languages enjoy a 1to1 correspondence between the syntactic right congruence of the language and the states of a minimal deterministic automaton (as articulated by the famous MyhillNerode theorem) such a correspondence is lacking from regular omegalanguages (regular languages of infinite words). This makes the problem of learning regular omegalanguages more intriguing. In this talk I will survey results on learning omegaregular languages, via several learning paradigms and using different canonical (or noncanonical) representations. 
15:00  15:30 
Automata and Coalgebras in Categories of Species
Preprint Slides
Abstract We study generalized automata (in the sense of AdámekTrnková) in Joyal's category of (setvalued) combinatorial species, and as an important preliminary step, we study coalgebras for its derivative endofunctor $\partial$ and for the `Euler homogeneity operator' $L\circ\partial$ arising from the adjunction $L\dashv\partial\dashv R$. 
15:30  16:00 
Automata in WToposes, and General MyhillNerode Theorems
Preprint Slides
Abstract We extend the functorial approach to automata by Colcombet and Petrisan from the category of sets to any Wtopos and establish general MyhillNerode theorems in our setting, including an explicit relationship between the syntactic monoid and the transition monoid of the minimal automaton. As a special case we recover the result of Bojanczyk, Klin and Lasota for orbitfinite nominal automata by considering automata in the MyhillSchanuel topos of nominal sets. 
16:00  16:30 
Coffee Break

16:30  17:00 
Effectful Trace Semantics: Extended Abstract
Preprint Slides
Abstract We introduce effectful streams, a coinductive semantic universe for effectful dataflow programming and traces. In monoidal categories with conditionals and ranges, we show that effectful streams particularize to families of morphisms satisfying a causality condition. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; we prove that bisimulation implies effectful trace equivalence. 
17:00  17:30 
Graded Semantics and Graded Logics for EilenbergMoore Coalgebras
Preprint Slides
Abstract Coalgebra, as the abstract study of statebased systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide with language equivalence. Language equivalence can be captured as behavioural equivalence on the determinization, which is obtained via the standard powerset construction. This construction can be lifted to coalgebraic generality, assuming a socalled EilenbergMoore distributive law between the functor determining the type of accepted structure (e.g. word languages) and a monad capturing the branching type (e.g. nondeterministic, weighted, probabilistic). EilenbergMoorestyle coalgebraic semantics in this sense has been shown to be essentially subsumed by the more general framework of graded semantics, which is centrally based on graded monads. Graded semantics comes with a range of generic results, in particular regarding invariance and, under suitable conditions, expressiveness of dedicated modal logics for a given semantics; notably, these logics are evaluated on the original state space. We show that the instantiation of such graded logics to the case of EilenbergMoorestyle semantics works extremely smoothly, and yields expressive modal logics in essentially all cases of interest. We additionally parametrize the framework over a quantale of truth values, thus in particular covering both the twovalued notions of equivalence and quantitative ones, i.e. behavioural distances. 
17:30  18:00 
On the Centre of Strong Graded Monads
Preprint Slides
Abstract We introduce the notion of “centre” for pomonoidgraded strong monads which generalizes some previous work that describes the centre of (not graded) strong monads. We show that, whenever the centre exists, this determines a pomonoidgraded commutative submonad of the original one. We also discuss how this relates to duoidallygraded strong monads. 
19:00  21:00 
Workshop Dinner at Restaurant Mamacita

Sunday, April 07, 2024
9:00  10:00 
Higher Coalgebra: A Homotopy Theory Of Behaviour (Invited Talk)
Slides
Abstract There is an intricate link between concurrent systems and homotopy theory, which has been exploited in the analysis of higherdimensional automata and distributed algorithms. The link between computation and homotopy theory goes even further and my longterm goal is to develop a general theory of higher coalgebras in the context of (∞, n)category theory for n ∈ {1,2}, which provides an abstract account of this link. (∞, 1)categories have various models, among them topologically and simplicially enriched categories. These are quite rigid models but they lend themselves to concrete computations (see Lurie's Higher Topos Theory).
In this talk, we will first develop some theory of higher coalgebra in quasicategories, which are a robust model of (∞,1)categories. In particular we will look at distributive laws and bisimilarity. We will then go to topologicallyenriched categories as an even more concrete model of (∞,1)categories, which is related to quasicategories via the homotopy coherent nerve. Particularly, we can easily study in this setting modal logic for hybrid systems that is invariant under homotopy. Hybrid systems will generally serve as a motivating example for homotopy theory throughout the talk. 
10:00  10:30 
Coffee Break

10:30  11:00 
Explicit Hopcroft’s Trick in Categorical Partition Refinement
Preprint
Abstract Algorithms for partition refinement are actively studied for a variety of systems, often with the optimisation called Hopcroft’s trick. However, the lowlevel description of those algorithms in the literature often obscures the essence of Hopcroft’s trick. Our contribution is twofold. Firstly, we present a novel formulation of Hopcroft’s trick in terms of general trees with weights. This clean and explicit formulation—we call it Hopcroft’s inequality—is crucially used in our second contribution, namely a general partition refinement algorithm that is functorgeneric (i.e. it works for a variety of systems such as (non)deterministic automata and Markov chains). Here we build on recent works on coalgebraic partition refinement but depart from them with the use of fibrations. In particular, our fibrational notion of Rpartitioning exposes a concrete tree structure to which Hopcroft’s inequality readily applies. It is notable that our fibrational framework accommodates such algorithmic analysis on the categorical level of abstraction. 
11:00  11:30 
Proving Behavioural Apartness
Preprint Slides
Abstract Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of statebased systems.
We propose \emph{behavioural apartness}, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples. 
11:30  12:00 
A Compositional Approach to Petri Nets
Preprint
Abstract We define a bidirectional compositional framework for Petri nets based on a line of work about compositionally defining games and computation models. This relies on defining structures with open ends that form interfaces they can be composed along. Together with this syntactic construction, we give a graphical language of morphisms in a PROP and a semantic category that describes the evolution of markings in a Petri net. Compared to previous work, the novelty is that computations in a Petri net are stateful, requiring specific care. We give algorithms to solve reachability compositionally in this framework. 
12:00  12:30 
Optics, Functorially
Preprint Slides
Abstract Optics are valuable categorical constructions encapsulating the general notion of bidirectional data access, and extensive research has been dedicated to comprehending these structures in recent years. Profunctor representation is a successful framework for encompassing various types of optics, such as lenses, prisms or traversals, starting from a pair of actions of a monoidal category. We enhance the above framework as to include structurepreserving functors of the two monoidal actions involved. This has the advantage of unifying within a single 2functorial framework not only optics (which usually are treated as arrows in categories), but also morphisms between them, and makes it convenient to manipulate and to reason about them in a uniform manner. From a more practical perspective, there is potential in developing better suited applications like complex data access schemes. 
12:30  14:00 
Lunch Break

Special Session: Coalgebras in Type Theory and Proof Assistants  
14:00  15:00 
Final Coalgebras of Finitary Functors in Type Theory
Abstract It is wellknown that the final coalgebras of polynomial functors can be constructed internally in constructive type theory, without the use of coinductive types. But what can be said about final coalgebras of finitary but nonpolynomial functors? In set theory there exist many different constructions for such objects, but are these replicable in a constructive setting without the assumption of classical principles? In this talk, we will work in homotopy type theory and inspect the cases of the finite powerset functor and the finite multiset functor, and generalizations of the latter to other analytic functors. We will investigate various constructions in categories whose objects generalize the notion of set: setoids (and pseudoequivalence relations), homotopy sets and homotopy groupoids. 
15:00  16:00 
Measuring Algebras by Coalgebras
Slides
Abstract In this talk, we focus on algebras and coalgebras of endofunctors (with a particular interest in polynomial endofunctors for defining co/inductive types). There are many interesting interactions between the algebras and coalgebras of a given endofunctor, but in this talk we focus on one in particular: the fact that (with some hypotheses) the category of algebras is enriched in the corresponding category of coalgebras. I will explain how this allows us to `measure' algebra homomorphisms and generalize the notion of initial algebras (and therefore inductive types). This is based on a recent paper (https://arxiv.org/abs/2303.16793). 
16:00  16:30 
Coffee Break

16:30  17:00 
Correspondence between Composite Theories and Distributive Laws
Preprint Slides
Abstract Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we describe when a minimal set of equations axiomatises the composite theory. 
17:00  17:30 
Finitary Traces in TwoPlayer Games
Preprint
Abstract This work gives an account of finitary coalgebraic trace semantics for twoplayer games. Systemversusenvironment games are modelled using composite monads, using full and weak distributive laws. These laws essentially swap an environmentthensystem branching into systemthenenvironment branching, by picking a onestep strategy for the system.
We consider both the Kleisli approach to defining finite traces
for generative systems, and the EMapproach to defining finite traces for reactive systems, and identify conditions under which these apply to the resulting
composite monads. Finally, we speculate on the role of strategies and the potential of generalising to infinite trace semantics.

17:30  18:00 
Category Theory for Compositional Verification
Preprint Slides
Abstract We present a recent line of work on open games, which describe compositional frawmeworks for games, in particular parity games and Markov decision processes. This is done by adding open ends that form interfaces along which two games can be composed. By finding adequate syntactic and semantic categories, we can then write algorithms that can leverage compositionality to compute faster solutions when there are repeated subgames.
Here, we show the categorical machinery at work in the definition of open parity games (OPGs) and related categories, as well as some particularities that arise in the case of open Markov decision processes (OMDPs). Our goal is to understand our main results and why they are relevant. We also show that it is possible to derive efficient algorithms from category theory. 