ETAPS 2022 Satellite Event

Programme

Warning: this timetable was generated automatically on
2022-05-13 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

Ana Sokolova

Trace semantics, also known as linear-time semantics, is the essential semantics of systems, programs, objects, seen as black boxes with some observable behaviour. Unlike its branching-time, step-wise 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

Samson Abramsky, Tomáš Jakl, Thomas Paine

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 Eilenberg-Moore 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-
binatorial and homomorphism-counting aspect of the theory (regardless
if any model comparison games are involved or not). We show that any
standard graph parameter has a corresponding comonad, classifying the
same class. This comonad is constructed via a simple Kan extension for-
mula, making it the initial solution to this problem and, furthermore,
automatically admitting a homomorphism-counting theorem.

11:00 – 11:30
Algebraic Presentation of Semifree Monads

Aloïs Rosset, Helle Hvid Hansen, Joerg Endrullis

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

Florian Frank, Stefan Milius, Henning Urbat

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. Bar-languages are sets of such words modulo
alpha-equivalence, and to every state of an RNNA one associates
its accepted bar-language. We show that this semantics arises both
as an instance of the Kleisli-style 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

Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, Alexandra Silva

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

Slawomir Lasota

I shall recall the model of register automata (RA), and relate it to the setting of orbit-finite 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 orbit-finite rational expressions (with orbit-finite 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

Mahsa Shirmohammadi

In this talk, I will discuss learning algorithms for weighted automata over principal ideal domains (PIDs). An example is Z-automata 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

Henning Urbat

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 orbit-finite 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

Thorsten Wißmann

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 well-known 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

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, Henning Urbat

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 fine-grained 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 coarse-grained semantics, respectively given by assuming read-only 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, Proof-search, and Coalgebra (Extended Abstract)

Alexander Gheorghiu, David Pym

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 proof-search. 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
No-go theorems for mixed distributive laws: extended abstract

Nihil Shah, Amin Karamlou

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 no-go 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 non-empty powerset monad.
This result is then generalised in several ways. First, we show that the prefix list comonad cannot distribute over any distribution or multiset monad parameterised by a semiring.

Finally, we provide conditions under which the existence of one distributive law implies the existence of another, allowing us to construct further no-go results via contrapositive arguments.
To the best of our knowledge these are the first instances of no-go theorems for mixed distributive laws.

19:00 – open
Workshop Dinner

Sunday, April 03, 2022

Chair: Barbara König
9:00 – 10:00
Invited Talk: Coalgebra meets Hybrid Systems

Renato Neves

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 cyber-physical 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 while-loops. As alluded above, we will see that hybrid systems deviate from standard notions of computer science in many aspects. For example, whilst classical while-loops give rise to a single divergence point, hybrid while-loops 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 up-to via Causal Transformations

Damien Pous, Jurriaan Rot, Ruben Turkenburg

Up-to 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 up-to 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 up-to techniques both for corecursive definitions and coinductive proofs.

11:00 – 11:30
Predicate and relation liftings and modal logics for coalgebras with side effects

Harsh Beohar, Barbara König, Sebastian Küpper, Christina Mika-Michalski

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 Eilenberg-Moore 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

Heinz-Peter Gumm, Mona Taheri

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

Lawrence Moss, Victoria Noquez

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 non-negative 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

Bart Jacobs

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 Lattice-Theoretic Essence of Property Directed Reachability Analysis

Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro Hasuo

We present LT-PDR, a lattice-theoretic generalization of Bradley’s property directed reachability analysis (PDR) algorithm. LT-PDR 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 LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.

14:45 – 15:00
Virtual talk

Differential 2-rigs

Fosco Loregian, Todd Trimble

We propose the notion of differential 2-rig, 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 2-rigs has a geometric flavour (for example, we prove that for every ⊗-monoid M ∈ ℝ, the derivative dM is a M-module), 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 2-rigs on a signature, and we prove various initiality results: for example, a certain category of colored species is the free differential 2-rig on a single generator.

Chair: Fabio Zanasi
15:00 – 16:00
Invited Talk: Coalgebraic methods in probability

Sam Staton

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

Measure-Theoretic Semantics for Quantitative, Linear-Time Logics

Corina Cirstea

We show that quantitative fixpoint logics for coalgebras with branching can be given an equivalent measure-theoretic 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 semiring-valued measures.

16:45 – 17:00
Boolean-Valued Multiagent Coalgebraic Logic

Alexander Kurz, Nima Motamed

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 two-valued logics via distributive laws to multiagent logics on (co-)Kleisli categories, thus giving a category-theoretic 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

Chase Ford, Stefan Milius, Lutz Schröder, Barbara König, Harsh Beohar

The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator 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 trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.