CMCS 2020 will be held over five online sessions in September-October 2020. Please find the programme below (this might still be subject to last-minute changes). In particular, we’re still planning discussion/social sessions, to be added to the programme. All times are in CEST.
In the programme you may find regular talks, invited talks, tutorial talks, and short contributions.
Monday 21 September 2020, Online
|15:00-16:00||Invited Talk: The Theory of Universal Graphs for Games: Past and Future
This paper surveys recent works about the notion of universal graphs. They were introduced in the context of parity games for understanding the recent quasipolynomial time algorithms, but they are defined for arbitrary objectives yielding a new approach for constructing efficient algorithms for solving different classes of games.
|16:30-17:00||Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas|
|17:00-17:30||Learning Automata with Side-Effects|
|17:30-18:00||Preservation of Algebraic Features by Monoidal Monads|
Monday 28 September 2020, Online
|10:00-11:00||Keynote Talk: Logic and Automata: a coalgebraic perspective
In Theoretical Computer Science, the area of Logic and Automata combines a rich mathematical theory with many applications in for instance the specification and verification of software. Of particular relevance in this area is the design of formal languages and derivation systems for describing and reasoning about nonterminating or ongoing behavior, and the study of such formalisms through the theory of automata operating on potentially infinite objects.
We will take a foundational approach towards these issues using insights from Universal Coalgebra and Coalgebraic Logic. Specifically, we will review the basic theory of coalgebraic modal fixpoint logic and its link with coalgebra automata – finite automata that operate on coalgebras. We will show that much of the theory linking logic and automata in the setting of streams, trees or transition systems, transfers to the coalgebraic level of generality, and we will argue that this theory is essentially coalgebraic in nature.
Topics that will be covered include closure properties of classes of coalgebra automata, expressive completeness results concerning fixpoint logics, and the design of sound and complete derivation systems for modal fixpoint logics. The key instruments in our analysis will be those of a coalgebraic modal signature and its associated one-step logic. As we will see, many results in the theory of logic and automata are ultimately grounded in fairly simple observations on the underlying one-step logic.
|11:30-12:00||Duality for Instantial Neighbourhood Logic via Coalgebra|
|12:00-12:30||Aproximate coalgebra homomorphisms and approximate solutions|
|12:30-13:00||Alternating Automata via Weak Distributive Laws|
Monday 5 October 2020, Online
|15:00-16:00||Tutorial on probabilistic couplings I|
|16:00-17:00||Tutorial on probabilistic couplings II
Abstract (Part I & II)
Probabilistic couplings are a powerful abstraction for verifying probabilistic
Couplings are well-known in the logic and verification literature, where they
This tutorial will survey recent techniques in program verification for building
|17:30-18:00||De Finetti’s Construction as a Categorical Limit|
Monday 12 October 2020, Online
|10:00-11:00||Hypernet Semantics and Robust Observational Equivalence
In semantics of programming languages, observational equivalence  is the fundamental and classical question, asking whether two program fragments have the same behaviour in any program context. Establishing observational equivalence is vital in validating compiler optimisation and refactoring, and there have been proposed proof methodologies for observational equivalence, such as logical relations [9, 10] and applicative bisimulations . A challenge is, however, to establish robustness of observational equivalence, namely to prove that observational equivalence is preserved by a language extension. In this talk I will discuss how hypernet semantics can be used to reason about such robustness. The semantics was originally developed for cost analysis of program execution , in particular for analysis of a trade-off between space and time efficiency. It has been used to model exotic programming features [2, 7] inspired by Google’s TensorFlow, a machine learning library, and also to design a dataflow programming language . In hypernet semantics, program execution is modelled as dynamic rewriting of a hypernet, that is, graph representation of a program. Inspired by Girard’s Geometry of Interaction , the rewriting process is notably guided and controlled by a dedicated object (token) of the graph. The use of graphs together with the token enables a direct proof of observational equivalence. The key step of the proof is to establish robustness of observational equivalence relative to language features, using step-wise reasoning enriched with the so-called up-to technique .
|11:30-12:00||Injective Objects and Fibered Codensity Liftings|
|12:00-12:30||A categorical approach to secure compilation|
|12:30-13:00||Divergences on Monads and Relational Liftings|
Monday 19 October 2020, Online
|10:00-10:30||Free-algebra functors from a coalgebraic perspective|
|10:30-11:00||Semantics for first-order affine inductive datatypes via slice categories|