20220513 09:44:01.141348 by thorsten.
Do not change the table manually because any change will
be overwritten sooner or later!!
In the programme you may find regular talks, invited talks, tutorial talks, and short contributions.
Days:  Saturday (Apr 02)  Sunday (Apr 03) 
Saturday, April 02, 2022
8:55 – 9:00 
Opening

Chair: Helle H. Hansen  
9:00 – 10:00 
Keynote Talk: Tracing coalgebras: a case for monads
Slides Abstract Trace semantics, also known as lineartime semantics, is the essential semantics of systems, programs, objects, seen as black boxes with some observable behaviour. Unlike its branchingtime, stepwise sisters, trace semantics provides the whole observable behaviour of a system. Trace semantics is hard to compute and originally seemed difficult to study coalgebraically. This talk will provide an overview of coalgebraic approaches to trace semantics, over the last fifteen years, focusing on transition systems and automata with effects. Monads play a crucial role in the study of traces, which I will highlight in all approaches using a class of examples. I will also mention some of the context of this exciting line of work that in my view enabled and supported the coalgebraic trace theories.

10:00 – 10:30 
Coffee Break

Chair: Thorsten Wißmann  
10:30 – 11:00 
Discrete density comonads and graph parameters
Game comonads have brought forth a new approach to study
ing finite model theory categorically. By semantically representing states of model comparison games, they allow expressing important logical and combinatorial properties in terms of their EilenbergMoore coalge bras. As a result, a number of known results from finite model theory (such as homomorphism counting theorems) have been formalised and parametrised by comonads, allowing for new results by simply swapping the comonad at hand. In this paper we look at the limits of the comonadic approach in the com 
11:00 – 11:30 
Algebraic Presentation of Semifree Monads
Monads and their composition via distributive laws have many applications in program semantics and functional programming. For many interesting monads, distributive laws fail to exist, and this has motivated investigations into weaker notions. In this line of research, Petrişan and Sarkis recently introduced a construction called the semifree monad in order to study semialgebras for a monad and weak distributive laws. In this paper, we prove that an algebraic presentation of the semifree monad M^s on a monad M can be obtained uniformly from an algebraic presentation of M. This result was conjectured by Petrişan and Sarkis. We also show that semifree monads are ideal monads, but that the semifree construction is not a monad transformer.

11:30 – 12:00 
Coalgebraic Language Semantics for Nominal Automata
This paper provides a coalgebraic approach to the language semantics
of regular nominal nondeterministic automata (RNNA), which were introduced in previous work. These automata feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNA are strings formed by ordinary letters and name binding letters. Barlanguages are sets of such words modulo alphaequivalence, and to every state of an RNNA one associates its accepted barlanguage. We show that this semantics arises both as an instance of the Kleislistyle coalgebraic trace semantics as well as an instance of the coalgebraic language semantics obtained via generalized determinization. On the way we revisit coalgebraic trace semantics in general and give a new compact proof for the main result in that theory stating that an initial algebra for a functor yields the terminal coalgebra for the Kleisli extension of the functor. Our proof requires fewer assumptions on the functor than all previous ones. 
12:00 – 12:30 
A Categorical Framework for Learning Generalised Tree Automata
Automata learning is a popular technique used to automatically construct an automaton model from queries.
Much research went into devising ad hoc adaptations of algorithms for different types of automata. The CALF project seeks to unify these using category theory in order to ease correctness proofs and guide the design of new algorithms. In this paper, we extend CALF to cover learning of algebraic structures that may not have a coalgebraic presentation. Furthermore, we provide a detailed algorithmic account of an abstract version of the popular L* algorithm, which was missing from CALF. We instantiate the abstract theory to a large class of Set functors, by which we recover for the first time practical tree automata learning algorithms from an abstract framework and at the same time obtain new algorithms to learn algebras of quotiented polynomial functors. 
12:30 – 14:00 
Lunch Break

Chair: Clemens Kupke  
14:00 – 15:00 
Invited Tutorial 1 on Data Languages: Some recent advances in register automata
Slides Abstract I shall recall the model of register automata (RA), and relate it to the setting of orbitfinite automata. Then I will mention two recent advances concerning language expressivity of different types of RA, together with remaining open problems.
First, two complementing languages of nondeterministic RA are recognized by a deterministic RA. For two such languages which are disjoint but not necessarily complementing, one may ask if there is a deterministic (resp. unambiguous) RA whose language separates the two. It is not known if existence of a deterministic separator is decidable, and it is not known if (but conjectured that) an unambiguous separator always exists. The second advance considers orbitfinite rational expressions (with orbitfinite unions in place of finite ones). While languages of nondeterministic RA are not definable by such rational expressions, their Parikh (commutative) images are conjectured to be so. This has been recently confirmed for automata (and grammars) with 1 register, but is still open in case of 2 registers. 
15:00 – 16:00 
Invited Tutorial 2 on Data Languages: Learning weighted automata over fields and principal ideal domains
Slides Abstract In this talk, I will discuss learning algorithms for weighted automata over principal ideal domains (PIDs). An example is Zautomata that can be seen as register automata with affine integer updates over integers. I start with discussing properties of the Hankel matrix of a weighted automaton. Then I reiterate briefly the idea behind learning weighted automata over fields. For automata over PIDs, I recall an existing algorithm (Heerdt et al., FoSSaCS 2020) for exact learning that has no complexity bounds (but only termination). I will recall a classical result of Fatou, and, inspired by its proof, draft a simpler learning algorithm for learning weighted automata over PIDs. I also briefly talk about learning algorithms for polynomial automata. I will conclude with mentioning that the automata I talk about can be seen as coalgebras. It will be interesting to see whether the learning algorithms can be simulated by general coalgebraic learning approaches.

16:00 – 16:30 
Coffee Break

Chair: Jurriaan Rot  
16:30 – 16:45 
Nominal Topology for Data Languages
The topological approach to classical regular languages rests on the observation that the free completion of finite sets under codirected limits is given by the category of Stone spaces. We present an extension of this result to bounded orbitfinite nominal sets, and outline some applications to the theory of data languages.

16:45 – 17:00 
Supported Sets – A New Foundation For Nominal Sets And Automata
This proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the wellknown abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a determinization process that takes the finite representation of a register automaton in supported sets and transforms it into its configuration automaton in nominal sets.

17:00 – 17:15 
Stateful Structural Operational Semantics
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very finegrained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarsegrained semantics, respectively given by assuming readonly interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

17:15 – 17:30 
Reductive Logic, Proofsearch, and Coalgebra (Extended Abstract)
The reductive, as opposed to deductive, view of logic is the form of logic that is, perhaps, most widely employed
in practical reasoning. Here we explore how coalgebraic semantics can be used to describe the concrete operational choices that are an essential part of proofsearch. This outlines a program to develop a uniform, generic, mathematical framework for understanding the relationship between the deductive structure of logics and the control structures of the corresponding reductive paradigm. 
17:30 – 17:45 
Nogo theorems for mixed distributive laws: extended abstract
Monads and comonads are important constructions of category theory which find widespread application in computer science and other related disciplines.
Distributive laws allow these constructions to interact compositionally. Such laws are not guaranteed to exist, and even when they do, finding them can be a difficult and time consuming task. Inspired by recent results which establish conditions under which no distributive laws can exist between pairs of monads, we present a family of nogo theorems for the existence of mixed distributive laws between a comonad and a monad. We begin by showing that in the category of sets the prefix list comonad cannot distribute over the nonempty powerset monad. Finally, we provide conditions under which the existence of one distributive law implies the existence of another, allowing us to construct further nogo results via contrapositive arguments. 
19:00 – open 
Workshop Dinner

Sunday, April 03, 2022
Chair: Barbara König  
9:00 – 10:00 
Invited Talk: Coalgebra meets Hybrid Systems
Slides Abstract A main challenge of the 21st century is to engineer software systems that tightly interact with physical processes such as velocity, movement, energy, and time. Such systems are qualified as ‘hybrid’ to emphasise this cyberphysical interaction – which remarkably forces a shift from standard software practices to a more multifaceted view that combines computer science, control theory, and analysis.
In this talk, I will discuss how Coalgebra can help advance hybrid systems theory. In particular, I will describe previous applications of Coalgebra to tackle two central problems in the field: the lack of a uniform framework for hybrid automata (currently, the standard formalism for hybrid systems) and the lack of suitable semantics for interpreting hybrid whileloops. As alluded above, we will see that hybrid systems deviate from standard notions of computer science in many aspects. For example, whilst classical whileloops give rise to a single divergence point, hybrid whileloops give rise to a whole continuum of divergence points. Nonetheless, we will see that Coalgebra can still properly guide us in providing a semantics for the latter kind of loop. I will conclude with a brief mention of other significant challenges in the field of hybrid systems and possible uses of Coalgebra to tackle them. 
10:00 – 10:30 
Coffee Break

Chair: Stefan Milius  
10:30 – 11:00 
Corecursion upto via Causal Transformations
Upto techniques are a widely used family of enhancements of corecursion and coinduction. The soundness of these techniques can be shown systematically through the use of distributive laws. In this paper we propose instead to present upto techniques as causal trans formations, which are a certain type of natural transformations over the final sequence of a functor. These generalise the approach to proving soundness via distributive laws, and inherit their good compositionality properties. We show how causal transformations give rise to valid upto techniques both for corecursive definitions and coinductive proofs.

11:00 – 11:30 
Predicate and relation liftings and modal logics for coalgebras with side effects
We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an EilenbergMoore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from a relation lifting (a special kind of indexed morphism) and we give a general recipe to construct such liftings in the above three cases. Lastly, we apply this framework to derive logical characterisations for (weighted) language equivalence and conditional bisimilarity.

11:30 – 12:00 
Virtual talk
Saturated Kripke Structures as Vietoris Coalgebras
We show that the category of coalgebras for the compact Vietoris endofunctor \mathbb{V} on the category Top of topological spaces and continuous mappings is isomorphic to the category of all modally saturated Kripke structures. Extending a result of Bezhanishvili, Fontaine and Venema, we show that Vietoris subcoalgebras as well as bisimulations admit topological closure and that the category of Vietoris coalgebras has a terminal object.

12:00 – 12:30 
Virtual talk
Corecursive Algebras in Nature
This paper continues the exploration of continuous mathematics from the point of view
of coalgebra, building on the original final coalgebra presentations due to Pavlovic and Pratt. We work with simple functors on the category of sets. We obtain Pavlovic and Pratt’s results and additional final coalgebra results by first finding corecursive algebra structures whose carriers sets of real numbers. These carriers include the set of nonnegative real numbers and the closed unit interval. The structure maps are simply defined functions. We derive a general result along those lines giving a sufficient condition for extracting a final coalgebra as a subalgebra of a corecursive algebra. This paper is part of a line of work investigating connections of continuous mathematics with topics found at CMCS and highlights connections to geometric series, fractal sets, and continued fractions. 
12:30 – 14:00 
Lunch Break

13:15 – 14:00 
Business meeting

Chair: Tobias Kappé  
14:00 – 14:30 
Virtual talk
Stick Breaking, in Coalgebra and Probability
Stick breaking is an elementary operation that has been formulated and
used within stochastic process theory. This paper extracts the essentials of stick breaking in terms of isomorphisms between discrete probability distributions (with full support) and sequences of numbers between zero and one. This works for both finite and infinite distributions. Stick breaking is a repetitive construction with a strong coalgebraic flavour. Indeed, we show that stick breaking turns the discrete distributions with infinite full support on the natural numbers into a final coalgebra. Once we have isolated stick breaking as a separate construction, we illustrate its usefulness in the description of various other probability distributions, such as binomial & multinomial and Beta & Dirichlet. 
14:30 – 14:45 
Virtual talk
The LatticeTheoretic Essence of Property Directed Reachability Analysis
We present LTPDR, a latticetheoretic generalization of Bradley’s property directed reachability analysis (PDR) algorithm. LTPDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster–Tarski and Kleene theorems. We introduce four concrete instances of LTPDR, derive their implementation from a generic Haskell implementation of LTPDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.

14:45 – 15:00 
Virtual talk
Differential 2rigs
We propose the notion of differential 2rig, a category ℝ equipped with coproducts and a monoidal structure distributing over them, also equipped with an endofunctor d : ℝ → ℝ that satisfies a categorified analogue of the Leibniz rule. This is intended as a tool to unify various applications of such categories to computer science, algebraic topology, and enumerative combinatorics. The theory of differential 2rigs has a geometric flavour (for example, we prove that for every ⊗monoid M ∈ ℝ, the derivative dM is a Mmodule), but boils down to a specialization of the theory of tensorial strengths on endofunctors, tightly connected to applicative endofunctors in functional programming, and captures the construction of Brzozowski derivatives in formal language theory. This builds a surprising connection between apparently disconnected fields. We provide an explicit construction to build free 2rigs on a signature, and we prove various initiality results: for example, a certain category of colored species is the free differential 2rig on a single generator.

Chair: Fabio Zanasi  
15:00 – 16:00 
Invited Talk: Coalgebraic methods in probability
Slides Abstract I will discuss some of the roles that coalgebra can play in probability theory and statistics. Infinite dimensional systems are often described as generative models, and these are often like coalgebras, as I will explain. I will look at some recent statistical models that involve symmetries, such as the “Chinese Restaurant process” and “Indian Buffet process”. Since these use names implicitly, I’ll connect this to nominal techniques. I will also discuss our probabilistic programming library “lazyppl”, which uses coinductive structures extensively.
I won’t assume much familiarity with probability, statistics, nominal techniques, or probabilistic programming. The talk will draw on joint work with Ackerman, Dash, Freer, Jacobs, Kaddar, Paquet, Roy, Sabok, Stein, Wolman, Yang, and others. 
16:00 – 16:30 
Coffee Break

Chair: Ana Sokolova  
16:30 – 16:45 
Virtual talk
MeasureTheoretic Semantics for Quantitative, LinearTime Logics
We show that quantitative fixpoint logics for coalgebras with branching can be given an equivalent measuretheoretic semantics, assigning to each formula and each state the measure of the set of paths from that state which satisfy the formula in the qualitative sense. Since branching is modelled using monads weighted in partial semirings, defining this semantics requires extending basic results in measure theory to semiringvalued measures.

16:45 – 17:00 
BooleanValued Multiagent Coalgebraic Logic
We study coalgebraic generalisations of Fitting’s multiagent semantics of modal logic from his article ‘How True It Is = Who Says It’s True’. First, we lift twovalued logics via distributive laws to multiagent logics on (co)Kleisli categories, thus giving a categorytheoretic account of Fitting’s notion of slicing. Second, we provide an alternative semantics where slicing is modelled in the functor instead of in the base category. Third, we extend our models to work with ordered sets of agents, and show that this enables the modelling of differences in expertise, certainty, and ability to achieve outcomes.

17:00 – 17:15 
Graded Monads and Behavioural Equivalence Games
The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the lineartime/branchingtime spectrum, over general system types. We describe a generic SpoilerDuplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for tracelike equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinitedepth graded semantics. Under reasonable restrictions, the infinitedepth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.
