Virtual Conference, September-October 2020

Programme

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

Nathanaël Fijalkow

Abstract
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:00-16:30 Break
16:30-17:00 Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas

Barbara König, Christina Mika-Michalski and Lutz Schröder

17:00-17:30 Learning Automata with Side-Effects

Gerco van Heerdt, Matteo Sammartino and Alexandra Silva

17:30-18:00 Preservation of Algebraic Features by Monoidal Monads

Louis Parlant

Abstract (pdf)

Monday 28 September 2020, Online

 

10:00-11:00 Keynote Talk: Logic and Automata: a coalgebraic perspective

Yde Venema

Abstract
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:00-11:30 Break
11:30-12:00 Duality for Instantial Neighbourhood Logic via Coalgebra

Nick Bezhanishvili, Sebastian Enqvist and Jim de Groot

12:00-12:30 Aproximate coalgebra homomorphisms and approximate solutions

Jiri Adamek

12:30-13:00 Alternating Automata via Weak Distributive Laws

Alexandre Goy

Abstract (pdf)

Monday 5 October 2020, Online

 

15:00-16:00 Tutorial on probabilistic couplings I

Justin Hsu

16:00-17:00 Tutorial on probabilistic couplings II

Marco Gaboardi

Abstract (Part I & II)

Probabilistic couplings are a powerful abstraction for verifying probabilistic
properties. Originating from probability theory, a coupling is a distribution
over pairs that relates—or couples—two given distributions. If we can find a
coupling with certain properties, then we can conclude properties about the two
related distributions. Moreover, couplings can be constructed compositionally,
a proof technique called “proof by coupling”.

Couplings are well-known in the logic and verification literature, where they
are called probabilistic bisimulations. Traditionally, bisimulations have been
used for verifying equivalence or refinement of finite state probabilistic
transition systems. However, the wide variety of proofs by coupling in
mathematics suggests that the technique can prove more sophisticated properties
for richer probabilistic computations, such as imperative programs and infinite
state systems.

This tutorial will survey recent techniques in program verification for building
and reasoning about probabilistic couplings. These methods have enabled the
first formal verification of probabilistic algorithms and properties that
previously seemed out of reach. The first half of the tutorial will cover
classical applications of coupling techniques, such as equivalence, convergence,
and stochastic ordering. The second half of the tutorial will cover approximate
couplings, an extension of the coupling method that has emerged in the program
verification literature to establish differential privacy.

17:00-17:30 Break
17:30-18:00 De Finetti’s Construction as a Categorical Limit

Bart Jacobs and Sam Staton

Monday 12 October 2020, Online

 

10:00-11:00 Hypernet Semantics and Robust Observational Equivalence

Koko Muroya

Abstract

In semantics of programming languages, observational equivalence [6] 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 [1]. 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 [8], 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 [3]. 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 [4], 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 [5].

References
1. Abramsky, S.: The lazy lambda-calculus, p. 65–117. Addison Wesley (1990)
2. Cheung, S.W.T., Darvariu, V., Ghica, D.R., Muroya, K., Rowe, R.N.S.: A functional perspective on machine learning via programmable induction and abduction. In: FLOPS 2018. Lect. Notes Comp. Sci., vol. 10818, pp. 84–98. Springer (2018).
https://doi.org/10.1007/978-3-319-90686-7 6
3. Cheung, S.W.T., Ghica, D.R., Muroya, K.: Transparent synchronous dataflow.
arXiv preprint arXiv:1910.09579 (2019)
4. Girard, J.Y.: Geometry of Interaction I: interpretation of system F. In: Logic Col-
loquium 1988. Studies in Logic & Found. Math., vol. 127, pp. 221–260. Elsevier (1989). https://doi.org/10.1016/S0049-237X(08)70271-4
5. Milner, R.: Communicating and mobile systems: the pi-calculus. Cambridge University Press (1999)
6. Morris Jr, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1969)
7. Muroya, K., Cheung, S.W.T., Ghica, D.R.: The geometry of computation-
graph abstraction. In: LICS 2018. pp. 749–758. ACM (2018). https://doi.org/10.1145/3209108.3209127
8. Muroya, K., Ghica, D.R.: The dynamic geometry of interaction machine: A tokenguided graph rewriter. LMCS 15(4) (2019), https://lmcs.episciences.org/5882
9. Plotkin,G.D.:Lambda-definabilityandlogicalrelations(1973),memorandumSAI-
RM-4
10. Statman, R.: Logical relations and the typed lambda-calculus. Information and
Control 65(2/3), 85–97 (1985). https://doi.org/10.1016/S0019-9958(85)80001-2

11:00-11:30 Break
11:30-12:00 Injective Objects and Fibered Codensity Liftings

Yuichi Komorida

12:00-12:30 A categorical approach to secure compilation

Stelios Tsampas, Andreas Nuyts, Dominique Devriese and Frank Piessens

12:30-13:00 Divergences on Monads and Relational Liftings

Tetsuya Sato and Shin-ya Katsumata

Abstract (pdf)

Monday 19 October 2020, Online

 

10:00-10:30 Free-algebra functors from a coalgebraic perspective

H. Peter Gumm

10:30-11:00 Semantics for first-order affine inductive datatypes via slice categories

Vladimir Zamdzhiev