Coalgebraic Methods in Computer Science

Daniela Petrişan, Jurriaan Rot

► To cite this version:

Daniela Petrişan, Jurriaan Rot. Coalgebraic Methods in Computer Science: 15th IFIP WG 1.3 International Workshop, CMCS 2020, Colocated with ETAPS 2020, Dublin, Ireland, April 25–26, 2020, Proceedings. Springer International Publishing, LNCS-12094, 2020, Lecture Notes in Computer Science, 978-3-030-57200-6. 10.1007/978-3-030-57201-3 . hal-03232344

HAL Id: hal-03232344

https://inria.hal.science/hal-03232344

Submitted on 3 Jul 2023

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Founding Editors

Gerhard Goos

Karlsruhe Institute of Technology, Karlsruhe, Germany

Juris Hartmanis

Cornell University, Ithaca, NY, USA

Editorial Board Members

Elisa Bertino

Purdue University, West Lafayette, IN, USA

Wen Gao

Peking University, Beijing, China

Bernhard Steffen

TU Dortmund University, Dortmund, Germany

Gerhard Woeginger

RWTH Aachen, Aachen, Germany

Moti Yung

Columbia University, New York, NY, USA
More information about this series at http://www.springer.com/series/7407
Daniela Petrişan · Jurriaan Rot (Eds.)

Coalgebraic Methods
in Computer Science

15th IFIP WG 1.3 International Workshop, CMCS 2020

Colocated with ETAPS 2020

Dublin, Ireland, April 25–26, 2020

Proceedings

<figure><img src="image_2.png" /></figure>

Springer
Editors

Daniela Petrișan

Université de Paris, CNRS, IRIF

Paris, France

Jurriaan Rot

Radboud University

Nijmegen, The Netherlands

ISSN 0302-9743

ISSN 1611-3349 (electronic)

Lecture Notes in Computer Science

ISBN 978-3-030-57200-6

ISBN 978-3-030-57201-3 (eBook)

https://doi.org/10.1007/978-3-030-57201-3

LNCS Sublibrary: SL1 – Theoretical Computer Science and General Issues

© IFIP International Federation for Information Processing 2020

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed.

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use.

The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland
# Preface

The 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2020) was originally planned to be held on April 25–26, 2020, in Dublin, Ireland, as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2020). Due to the 2020 COVID-19 pandemic, it was canceled, and held in alternative form as a series of online seminars, ranging over several weeks in the fall of 2020.

The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras, their logics, and their applications. Coalgebras allow for a uniform treatment of a large variety of state-based dynamical systems, such as transition systems, automata (including weighted and probabilistic variants), Markov chains, and game-based systems. Over the last two decades, coalgebra has developed into a field of its own interest, presenting a deep mathematical foundation, a growing field of applications, and interactions with various other fields such as reactive and interactive system theory, object-oriented and concurrent programming, formal system specification, modal and description logics, artificial intelligence, dynamical systems, control systems, category theory, algebra, analysis, etc.

Previous workshops of the CMCS series were held in Lisbon (1998), Amsterdam (1999), Berlin (2000), Genova (2001), Grenoble (2002), Warsaw (2003), Barcelona (2004), Vienna (2006), Budapest (2008), Paphos (2010), Tallinn (2012), Grenoble (2014), Eindhoven (2016), and Thessaloniki (2018). Since 2004, CMCS has been a biennial workshop, alternating with the International Conference on Algebra and Coalgebra in Computer Science (CALCO).

The CMCS 2020 program featured a keynote talk by Yde Venema (ILLC, University of Amsterdam, The Netherlands), an invited talk by Nathanaël Fijalkow (CNRS, LaBRI, University of Bordeaux, France), and an invited talk by Koko Muroya (RIMS, Kyoto University, Japan). In addition, a special session on probabilistic couplings was planned, featuring invited tutorials by Marco Gabardi (Boston University, USA) and Justin Hsu (University of Wisconsin-Madison, USA). This volume contains revised regular contributions (9 papers were accepted out of 13 submissions; 1 submission was conditionally accepted but unfortunately had to be rejected ultimately as the author did not agree to implement the changes required by the Program Committee) and the abstracts of 3 keynote/invited talks. All regular contributions were refereed by three reviewers. We wish to thank all the authors who submitted to CMCS 2020, and the external reviewers and the Program Committee members for their thorough reviewing and help in improving the papers accepted at CMCS 2020.

July 2020

Daniela Petrișan
Jurriaan Rot
## Organization

### Program Committee Chairs

Daniela Petrișan

Université de Paris, CNRS, IRIF, France

Jurriaan Rot

Radboud University, The Netherlands

### Steering Committee

Filippo Bonchi

University of Pisa, Italy

Marcello Bonsangue

CWI/Leiden University, The Netherlands

Corina Cîrstea

University of Southampton, UK

Ichiro Hasuo

National Institute of Informatics, Japan

Bart Jacobs

Radboud University, The Netherlands

Bartek Klin

University of Warsaw, Poland

Alexander Kurz

Chapman University, USA

Marina Lenisa

University of Udine, Italy

Stefan Milius (Chair)

FAU Erlangen-Nürnberg, Germany

Larry Moss

Indiana University, USA

Dirk Pattinson

The Australian National University, Australia

Lutz Schröder

FAU Erlangen-Nürnberg, Germany

Alexandra Silva

University College London, UK

### Program Committee

Henning Basold

Leiden University, The Netherlands

Nick Bezhanishvili

University of Amsterdam, The Netherlands

Corina Cîrstea

University of Southampton, UK

Mai Gehrke

CNRS and Université Côte d'Azur, France

Helle Hvid Hansen

Delft University of Technology, The Netherlands

Shin-Ya Katsumata

National Institute of Informatics, Japan

Bartek Klin

Warsaw University, Poland

Ekaterina Komendantskaya

Heriot-Watt University, UK

Barbara König

Universität Duisburg-Essen, Germany

Dexter Kozen

Cornell University, USA

Clemens Kupke

University of Strathclyde, UK

Alexander Kurz

Chapman University, USA

Daniela Petrișan

Université de Paris, France

Andrei Popescu

Middlesex University London, UK

Damien Pous

CNRS, ENS Lyon, France

Jurriaan Rot

Radboud University, The Netherlands

Davide Sangiorgi

University of Bologna, Italy
## Additional Reviewers

Alexandre Goy

Gerco van Heerdt

Stefan Milius

Laureline Pinault

Luigi Santocanale

## Sponsoring Institutions

IFIP WG 1.3

Logical Methods in Computer Science e.V.
Abstracts of Invited Talks
# Logic and Automata: A Coalgebraic Perspective

Yde Venema

Institute for Logic, Language and Computation, Universiteit van Amsterdam

y.venema@uva.nl

https://staff.fnwi.uva.nl/y.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.

**Keywords:** Coalgebra · Modal logic · Fixed points · Automata
# The Theory of Universal Graphs for Games:
## Past and Future

Nathanaël Fijalkow<fnref n="1" />,<fnref n="2" />

**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 quasip polynomial time algorithms, but they are defined for arbitrary objectives yielding a new approach for constructing efficient algorithms for solving different classes of games.

**Keywords:** Games · Parity games · Universal graphs

<footnote n="1">¹ CNRS, LaBRI, Université de Bordeaux, Bordeaux, France
nathanael.fijalkow@labri.fr</footnote>

<footnote n="2">² The Alan Turing Institute of Data Science, London, UK</footnote>
# Hypernet Semantics and Robust Observational Equivalence

Koko Muroya

RIMS, Kyoto University, Kyoto, Japan

kmuroya@kurims.kyoto-u.ac.jp

**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<fnref n="1" />, 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, pp. 65–117. Addison Wesley (1990)

2. Cheung, S., Darvariu, V., Ghica, D.R., Muroya, K., Rowe, R.N.S.: A functional perspective on machine learning via programmable induction and abduction. In: Gallagher, J., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818. Springer, Cham (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 Colloquium 1988. Studies in Logic and the Foundations of Mathematics, vol. 127, pp. 221–260. Elsevier (1989). https://doi.org/10.1016/S0049-237X(08)70271-4

<footnote n="1">¹ https://www.tensorow.org/.</footnote>
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 token-guided graph rewriter. LMCS 15(4) (2019). https://lmcs.episciences.org/5882

9. Plotkin, G.D.: Lambda-Definability and Logical Relations. Memorandum SAI-RM-4 (1973)

10. Statman, R.: Logical relations and the typed lambda-calculus. Inf. Control 65(2/3), 85–97 (1985). https://doi.org/10.1016/S0019-9958(85)80001-2
# Contents

<table><tr><td>The Theory of Universal Graphs for Games: Past and Future</td><td>1</td></tr><tr><td>Nathanaël Fijalkow</td><td></td></tr><tr><td>Approximate Coalgebra Homomorphisms and Approximate Solutions</td><td>11</td></tr><tr><td>Jiří Adámek</td><td></td></tr><tr><td>Duality for Instantial Neighbourhood Logic via Coalgebra</td><td>32</td></tr><tr><td>Nick Bezhanishvili, Sebastian Enqvist, and Jim de Groot</td><td></td></tr><tr><td>Free-Algebra Functors from a Coalgebraic Perspective.</td><td>55</td></tr><tr><td>H. Peter Gumm</td><td></td></tr><tr><td>Learning Automata with Side-Effects.</td><td>68</td></tr><tr><td>Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva</td><td></td></tr><tr><td>De Finetti's Construction as a Categorical Limit</td><td>90</td></tr><tr><td>Bart Jacobs and Sam Staton</td><td></td></tr><tr><td>Injective Objects and Fibered Codensity Liftings.</td><td>112</td></tr><tr><td>Yuichi Komorida</td><td></td></tr><tr><td>Explaining Non-bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas</td><td>133</td></tr><tr><td>Barbara König, Christina Mika-Michalski, and Lutz Schröder</td><td></td></tr><tr><td>A Categorical Approach to Secure Compilation</td><td>155</td></tr><tr><td>Stelios Tsampas, Andreas Nuyts, Dominique Devriese, and Frank Piessens</td><td></td></tr><tr><td>Semantics for First-Order Affine Inductive Data Types via Slice Categories.</td><td>180</td></tr><tr><td>Vladimir Zamdzhiev</td><td></td></tr><tr><td>Author Index</td><td>201</td></tr></table>