Programme

The schedule consists of regular talks, short contributions, and invited talks.

Warning: this timetable was generated automatically on 2024-04-25 10:38:41.594905 by an unknown person. Do not change the table manually because any change will be overwritten sooner or later!!

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) Shin-ya Katsumata 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 codensity-lifted functors.
10:00 - 10:30	Coffee Break
10:30 - 11:00	Coalgebraic CTL: Fixpoint Characterization and Polynomial-Time Model Checking Ryota Kojima, Corina Cirstea, Koko Muroya, Ichiro Hasuo Preprint Slides Abstract We introduce a path-based 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 path-based semantics of CCTL, and show how to encode this logic into a coalgebraic fixpoint logic with a step-wise semantics. Our main result shows that this encoding is semantics-preserving. We also present a polynomial-time model-checking algorithm for CCTL, inspired by the standard model-checking 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 mu-calculus. This categorical perspective also explains the absence of a similar encoding of PCTL (Probabilistic CTL) into the probabilistic mu-calculus.
11:00 - 11:30	A Categorical Approach to Coalgebraic Fixpoint Logic Ezra Schoen, Clemens Kupke, Jurriaan Rot, Ruben Turkenburg Preprint Slides Abstract We define a framework for incorporating fixpoint logics into the dual-adjunction setup for coalgebraic modal logics. We achieve this by using order-enriched categories. We give a least-solution semantics as well as an initial-algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic mu-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.
11:30 - 12:00	Preorder-Constrained Simulations for Program Refinement with Effects Koko Muroya, Takahiro Sanada, Natsuki Urabe Preprint Slides Abstract We propose a notion of preorder-constrained 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. Preorder-constrained simulation is additionally parameterised by a positive number ("look-ahead bound"), and forms a generative spectrum governed by the look-ahead bound. We analyse the complexity of determining preorder-constrained similarity, and show that preorder-constrained simulation can be enhanced by the so-called up-to technique.
12:00 - 12:30	Coinductive Reasoning about CRDT Emulation Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, Lindsey Kuper Preprint Slides Abstract Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs have historically been taxonomized into operation-based (or op-based) CRDTs and state-based CRDTs. The notion that state-based and op-based 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 state-based CRDT from a given op-based 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 Omega-Regular Languages - A Tour via Learning Paradigms and Canonical Representations (Invited Talk) Dana Fisman Abstract While regular languages enjoy a 1-to-1 correspondence between the syntactic right congruence of the language and the states of a minimal deterministic automaton (as articulated by the famous Myhill-Nerode theorem) such a correspondence is lacking from regular omega-languages (regular languages of infinite words). This makes the problem of learning regular omega-languages more intriguing. In this talk I will survey results on learning omega-regular languages, via several learning paradigms and using different canonical (or non-canonical) representations.
15:00 - 15:30	Automata and Coalgebras in Categories of Species Fosco Loregian Preprint Slides Abstract We study generalized automata (in the sense of Adámek-Trnková) in Joyal's category of (set-valued) 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 W-Toposes, and General Myhill-Nerode Theorems Victor Iwaniack Preprint Slides Abstract We extend the functorial approach to automata by Colcombet and Petrisan from the category of sets to any W-topos and establish general Myhill-Nerode 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 orbit-finite nominal automata by considering automata in the Myhill-Schanuel topos of nominal sets.
16:00 - 16:30	Coffee Break
16:30 - 17:00	Effectful Trace Semantics: Extended Abstract Filippo Bonchi, Elena Di Lavore, Mario Román 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 Eilenberg-Moore Coalgebras Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Karla Messing Preprint Slides Abstract Coalgebra, as the abstract study of state-based 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 so-called Eilenberg-Moore 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). Eilenberg-Moore-style 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 Eilenberg-Moore-style 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 two-valued notions of equivalence and quantitative ones, i.e. behavioural distances.
17:30 - 18:00	On the Centre of Strong Graded Monads Flavien Breuvart, Quan Long, Vladimir Zamdzhiev Preprint Slides Abstract We introduce the notion of “centre” for pomonoid-graded 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 pomonoid-graded commutative submonad of the original one. We also discuss how this relates to duoidally-graded 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) Henning Basold Slides Abstract There is an intricate link between concurrent systems and homotopy theory, which has been exploited in the analysis of higher-dimensional automata and distributed algorithms. The link between computation and homotopy theory goes even further and my long-term 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 topologically-enriched 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 Takahiro Sanada, Ryota Kojima, Yuichi Komorida, Koko Muroya, Ichiro Hasuo Preprint Abstract Algorithms for partition refinement are actively studied for a variety of systems, often with the optimisation called Hopcroft’s trick. However, the low-level 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 functor-generic (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 R-partitioning 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 Ruben Turkenburg, Harsh Beohar, Clemens Kupke, Jurriaan Rot 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 state-based 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 Serge Lechenne, Clovis Eberhart, Ichiro Hasuo 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 Adriana Balan, Silviu-George Pantelimon 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 structure-preserving functors of the two monoidal actions involved. This has the advantage of unifying within a single 2-functorial 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 Niccolò Veltri Abstract It is well-known 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 non-polynomial 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 pseudo-equivalence relations), homotopy sets and homotopy groupoids.
15:00 - 16:00	Measuring Algebras by Coalgebras Paige Randall North 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 Aloïs Rosset, Maaike Zwart, Helle Hvid Hansen, Joerg Endrullis 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 Two-Player Games Benjamin Plummer Preprint Abstract This work gives an account of finitary coalgebraic trace semantics for two-player games. System-versus-environment games are modelled using composite monads, using full and weak distributive laws. These laws essentially swap an environment-then-system branching into system-then-environment branching, by picking a one-step strategy for the system. We consider both the Kleisli approach to defining finite traces for generative systems, and the EM-approach 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 Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo 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 sub-games. 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.