Volume
LIPIcs, Volume 342
11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Publication Details
- published at: 2025-07-28
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-383-6
- DBLP: db/conf/calco/calco2025
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 342, CALCO 2025, Complete Volume
Abstract
LIPIcs, Volume 342, CALCO 2025, Complete Volume
Cite as
11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 1-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{cirstea_et_al:LIPIcs.CALCO.2025,
title = {{LIPIcs, Volume 342, CALCO 2025, Complete Volume}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {1--292},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025},
URN = {urn:nbn:de:0030-drops-241021},
doi = {10.4230/LIPIcs.CALCO.2025},
annote = {Keywords: LIPIcs, Volume 342, CALCO 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cirstea_et_al:LIPIcs.CALCO.2025.0,
author = {C\^{i}rstea, Corina and Knapp, Alexander},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.0},
URN = {urn:nbn:de:0030-drops-241005},
doi = {10.4230/LIPIcs.CALCO.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Effectful Mealy Machines: Coalgebraic and Causal Traces (Invited Talk)
Abstract
We introduce effectful Mealy machines - a general notion of Mealy machine with global effects - and give them semantics in terms of both bisimilarity and traces. Bisimilarity of effectful Mealy machines is characterized syntactically, via free uniform feedback. Their traces are given a novel semantic coinductive universe in terms of effectful streams. We prove that this framework generalizes standard causal processes and captures existing flavours of Mealy machine, bisimilarity, and trace.
This is an extended abstract for the manuscript Effectful Mealy Machines: Bisimulation and Trace that will appear in the proceedings of LiCS 2025 [Bonchi et al., 2025]; an extended version with proofs is also available (arxiv.org/abs/2410.10627) [Bonchi et al., 2025]. We additionally characterise causal processes as lax-natural transformations.
Cite as
Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy Machines: Coalgebraic and Causal Traces (Invited Talk). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2025.1,
author = {Bonchi, Filippo and Di Lavore, Elena and Rom\'{a}n, Mario},
title = {{Effectful Mealy Machines: Coalgebraic and Causal Traces}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {1:1--1:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.1},
URN = {urn:nbn:de:0030-drops-235596},
doi = {10.4230/LIPIcs.CALCO.2025.1},
annote = {Keywords: Mealy machines, coinduction, copy-discard categories, premonoidal categories}
}
Document
Invited Talk
Logic Enriched over a Quantale (Invited Talk)
Abstract
Many-valued logics have a long history in mathematical logic as well as in applications to the semantics of programming languages and to engineering more generally. Typically these logics are rich with features motivated by the particular applications they stem from. In his 1973 article "Metric Spaces, Generalized Logic, and Closed Categories", Lawvere argued that any quantale Ω gives rise to a generalized Ω-valued logic that has as its models the categories enriched over the quantale. This suggests developing a uniform framework for many-valued logics parameterized in a quantale. In this talk we will review some previous and ongoing work in that direction. In particular, we will address (not necessarily answer) the following questions.
- If we take as our starting point, generalizing from 2-valued lattice logic, a logical language that comprises not only meets and joins (limits and colimits) but also tensor and power (weighted limits and colimits), what laws do these operations satisfy?
- This question can be investigated for different types of semantics, generalizing the set-theoretic and the polarity-based semantics known from the 2-valued setting.
- Which additional properties obtain if the quantale is integral or commutative or finite or distributive, etc?
- On the other hand, quantale logics can also be investigated from a purely proof theoretic point of view, leading us to consider sequent calculi with turnstiles ⊢_ω labelled by elements ω ∈ Ω.
- As Galatos and Jipsen showed, there are 1662 "Residuated Lattices of Size up to 6". Each of them generates a different and potentially interesting logic.
- The adjunction Ω^-⊣ Ω^-:Ω-cat^op → Ω-cat exists for any quantale Ω. What is the logic enshrined in the monad of that adjunction? How far can one extend this to a theory of Stone duality for quantale logics parametric in the quantale?
- The Dedekind-MacNeille completion generalizes to quantale categories. Similarly, the theory of canonical extensions originating with Jonsson and Tarski (and important for completeness proofs of modal logics) can be extended to quantale logics.
- Since the discrete functor Set → Ω-cat is dense in the sense of Kelly, set-functors (equipped with an Ω-cat structure or not) can be extended to quantale categories via enriched left Kan extensions. This gives rise to a uniform variety of type constructors (endofunctors) on quantale categories parameterised by the quantale.
- Each endofunctor on Ω-cat gives rise to a category of coalgebras with their own notion of behavioural equivalence. How many of the existing notions of many-valued (probabilistic, metric, fuzzy, etc) bisimulation can be accounted for in this uniform framework?
- Morphism between quantales gives rise to change-of-base principles between categories of (co)algebras. Which transfer principles can be obtained from a systematic investigation of change of base for quantale categories?
- Exploiting the duality of coalgebras (as models of computation) and algebras (as modal logics), which general logical theory of computation arises from putting the items in this list together?
Cite as
Alexander Kurz. Logic Enriched over a Quantale (Invited Talk). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kurz:LIPIcs.CALCO.2025.2,
author = {Kurz, Alexander},
title = {{Logic Enriched over a Quantale}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.2},
URN = {urn:nbn:de:0030-drops-235609},
doi = {10.4230/LIPIcs.CALCO.2025.2},
annote = {Keywords: Modal Logic, Coalgebra, Enriched Category Theory}
}
Document
Terminal Coalgebras for Finitary Functors
Abstract
We present a result that implies that an endofunctor on a category has a terminal coalgebra obtainable as a countable limit of its terminal-coalgebra sequence. It holds for finitary endofunctors preserving nonempty binary intersections on locally finitely presentable categories, assuming that the posets of strong quotients and subobjects of every finitely presentable object satisfy the descending chain condition. This allows one to adapt finiteness arguments that were originally advanced by Worrell concerning terminal coalgebras for finitary set functors. Examples include the categories of sets, posets, vector spaces, graphs, and nominal sets. A similar argument is presented for the category of metric spaces (although it is not locally finitely presentable).
Cite as
Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Terminal Coalgebras for Finitary Functors. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2025.3,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
title = {{Terminal Coalgebras for Finitary Functors}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {3:1--3:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.3},
URN = {urn:nbn:de:0030-drops-235623},
doi = {10.4230/LIPIcs.CALCO.2025.3},
annote = {Keywords: terminal coalgebra, countable iteration, descending chain condition}
}
Document
Distributive Laws of Monadic Containers
Abstract
Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose.
In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu’s characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the "zoo" of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.
Cite as
Chris Purdy and Stefania Damato. Distributive Laws of Monadic Containers. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{purdy_et_al:LIPIcs.CALCO.2025.4,
author = {Purdy, Chris and Damato, Stefania},
title = {{Distributive Laws of Monadic Containers}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {4:1--4:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.4},
URN = {urn:nbn:de:0030-drops-235633},
doi = {10.4230/LIPIcs.CALCO.2025.4},
annote = {Keywords: distributive laws, monadic containers, monads, dependent types, cubical agda}
}
Document
String Diagrams for Graded Monoidal Theories, with an Application to Imprecise Probability
Abstract
We introduce string diagrams for graded symmetric monoidal categories. Our approach includes a definition of graded monoidal theory and the corresponding freely generated syntactic category. Also, we show how an axiomatic presentation for the graded theory may be modularly obtained from one for the grading theory and one for the base category. The Para construction on monoidal actegories is a motivating example for our framework. As a case study, we show how to axiomatise a variant of the graded category ImP, recently introduced by Liell-Cock and Staton to model imprecise probability [Liell-Cock and Staton, 2025]. This culminates in a representation, as string diagrams with grading wires, of programs with primitives for nondeterministic and probabilistic choices and conditioning.
Cite as
Ralph Sarkis and Fabio Zanasi. String Diagrams for Graded Monoidal Theories, with an Application to Imprecise Probability. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sarkis_et_al:LIPIcs.CALCO.2025.5,
author = {Sarkis, Ralph and Zanasi, Fabio},
title = {{String Diagrams for Graded Monoidal Theories, with an Application to Imprecise Probability}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {5:1--5:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.5},
URN = {urn:nbn:de:0030-drops-235641},
doi = {10.4230/LIPIcs.CALCO.2025.5},
annote = {Keywords: string diagrams, graded categories, probability, nondeterminism}
}
Document
An Algebraic Approach to Moralisation and Triangulation of Probabilistic Graphical Models
Abstract
Moralisation and Triangulation are transformations allowing to switch between different ways of factoring a probability distribution into a graphical model. Moralisation allows to view a Bayesian network (a directed model) as a Markov network (an undirected model), whereas triangulation works in the opposite direction. We present a categorical framework where these transformations are modelled as functors between a category of Bayesian networks and one of Markov networks. The two kinds of network (the objects of these categories) are themselves represented as functors, from a "syntax" domain to a "semantics" codomain. Notably, moralisation and triangulation are definable inductively on such syntax, and operate as a form of functor pre-composition. This approach introduces a modular, algebraic perspective in the theory of probabilistic graphical models.
Cite as
Antonio Lorenzin and Fabio Zanasi. An Algebraic Approach to Moralisation and Triangulation of Probabilistic Graphical Models. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lorenzin_et_al:LIPIcs.CALCO.2025.6,
author = {Lorenzin, Antonio and Zanasi, Fabio},
title = {{An Algebraic Approach to Moralisation and Triangulation of Probabilistic Graphical Models}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.6},
URN = {urn:nbn:de:0030-drops-235654},
doi = {10.4230/LIPIcs.CALCO.2025.6},
annote = {Keywords: Functorial Semantics, Probabilistic Model, Bayesian Network}
}
Document
A Coinductive Representation of Computable Functions
Abstract
We investigate a representation of computable functions as total functions over 2^∞, the set of finite and infinite sequences over {0,1}. In this model, infinite sequences are interpreted as non-terminating computations whilst finite sequences represent the sum of their digits. We introduce a new definition principle, function space corecursion, that simultaneously generalises minimisation and primitive recursion. This defines the class of computable corecursive functions that is closed under composition and function space corecursion. We prove computable corecursive functions represent all partial recursive functions, and show that all computable corecursive functions are indeed computable by translation into the untyped λ-calculus.
Cite as
Alvin Tang and Dirk Pattinson. A Coinductive Representation of Computable Functions. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{tang_et_al:LIPIcs.CALCO.2025.7,
author = {Tang, Alvin and Pattinson, Dirk},
title = {{A Coinductive Representation of Computable Functions}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.7},
URN = {urn:nbn:de:0030-drops-235662},
doi = {10.4230/LIPIcs.CALCO.2025.7},
annote = {Keywords: Computability, Coinduction}
}
Document
Drawing and Recolouring
Abstract
Drawing a ball from an urn filled with balls of different colours is one of the basic models in probability theory. The probability of drawing a ball of a particular colour is determined by the proportion / fraction of balls of that colour. This paper introduces a new stochastic model for such urns: draw a ball, recolour (repaint) it, and put it back into the urn. One can distinguish four modes of drawing-and-recolouring, namely whether done proportionally or uniformly (both for drawing and recolouring). These modes can be reformulated in financial terms as redistribution of wealth or in biological terms as evolutionary drift. The resulting four operations form a coalgebra for the distribution monad, on the set of multisets of a fixed size. In fact they form a Markov chain and even a hidden Markov model, in combination with the frequentist learning map as emission channel. This paper identifies fixed points, capturing stable situations, for these four modes of drawing-and-recolouring.
Cite as
Bart Jacobs and Márk Széles. Drawing and Recolouring. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jacobs_et_al:LIPIcs.CALCO.2025.8,
author = {Jacobs, Bart and Sz\'{e}les, M\'{a}rk},
title = {{Drawing and Recolouring}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {8:1--8:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.8},
URN = {urn:nbn:de:0030-drops-235674},
doi = {10.4230/LIPIcs.CALCO.2025.8},
annote = {Keywords: Markov-chain, Urn model, Multiset}
}
Document
Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics
Abstract
We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra 𝐀 of truth-degrees. More precisely, we work with coalgebraic modal logic via 𝐀-valued predicate liftings where 𝐀 is an FLew-algebra, and interpret actions (abstracting programs and games) as 𝖥-coalgebras where the functor 𝖥 represents some type of 𝐀-weighted system. We also allow combinations of crisp propositions with 𝐀-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 𝟐-valued iteration-free PDL with 𝐀-valued accessibility relations when 𝐀 is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.
Cite as
Helle Hvid Hansen and Wolfgang Poiger. Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hansen_et_al:LIPIcs.CALCO.2025.9,
author = {Hansen, Helle Hvid and Poiger, Wolfgang},
title = {{Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {9:1--9:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.9},
URN = {urn:nbn:de:0030-drops-235681},
doi = {10.4230/LIPIcs.CALCO.2025.9},
annote = {Keywords: dynamic logic, many-valued coalgebraic logic, safety, strong completeness}
}
Document
EGGs Are Adhesive!
Abstract
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders precise the properties of the data structure, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.
Cite as
Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs Are Adhesive!. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{biondo_et_al:LIPIcs.CALCO.2025.10,
author = {Biondo, Roberto and Castelnovo, Davide and Gadducci, Fabio},
title = {{EGGs Are Adhesive!}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.10},
URN = {urn:nbn:de:0030-drops-235690},
doi = {10.4230/LIPIcs.CALCO.2025.10},
annote = {Keywords: Hypergraphs, terms graphs, e-graphs, adhesive categories}
}
Document
Tape Diagrams for Monoidal Monads
Abstract
Tape diagrams provide a graphical representation for arrows of rig categories, namely categories equipped with two monoidal structures, ⊕ and ⊗, where ⊗ distributes over ⊕. However, their applicability is limited to categories where ⊕ is a biproduct, i.e., both a categorical product and a coproduct. In this work, we extend tape diagrams to deal with Kleisli categories of symmetric monoidal monads, presented by algebraic theories.
Cite as
Filippo Bonchi, Cipriano Junior Cioffo, Alessandro Di Giorgio, and Elena Di Lavore. Tape Diagrams for Monoidal Monads. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CALCO.2025.11,
author = {Bonchi, Filippo and Cioffo, Cipriano Junior and Di Giorgio, Alessandro and Di Lavore, Elena},
title = {{Tape Diagrams for Monoidal Monads}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {11:1--11:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.11},
URN = {urn:nbn:de:0030-drops-235703},
doi = {10.4230/LIPIcs.CALCO.2025.11},
annote = {Keywords: rig categories, string diagrams, monads, probabilistic control}
}
Document
Cancellative Convex Semilattices
Abstract
Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad.
A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations).
We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).
Cite as
Ana Sokolova and Harald Woracek. Cancellative Convex Semilattices. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sokolova_et_al:LIPIcs.CALCO.2025.12,
author = {Sokolova, Ana and Woracek, Harald},
title = {{Cancellative Convex Semilattices}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.12},
URN = {urn:nbn:de:0030-drops-235714},
doi = {10.4230/LIPIcs.CALCO.2025.12},
annote = {Keywords: convex semilattice, cancellativity, Riesz space}
}
Document
Expressivity of Bisimulation Pseudometrics over Analytic State Spaces
Abstract
A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.
Cite as
Daniel Luckhardt, Harsh Beohar, and Clemens Kupke. Expressivity of Bisimulation Pseudometrics over Analytic State Spaces. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{luckhardt_et_al:LIPIcs.CALCO.2025.13,
author = {Luckhardt, Daniel and Beohar, Harsh and Kupke, Clemens},
title = {{Expressivity of Bisimulation Pseudometrics over Analytic State Spaces}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {13:1--13:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.13},
URN = {urn:nbn:de:0030-drops-235727},
doi = {10.4230/LIPIcs.CALCO.2025.13},
annote = {Keywords: Markov decision process, quantitative Hennessy-Milner theorem}
}
Document
Pareto Fronts for Compositionally Solving String Diagrams of Parity Games
Abstract
Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure.
Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.
Cite as
Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{watanabe:LIPIcs.CALCO.2025.14,
author = {Watanabe, Kazuki},
title = {{Pareto Fronts for Compositionally Solving String Diagrams of Parity Games}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.14},
URN = {urn:nbn:de:0030-drops-235734},
doi = {10.4230/LIPIcs.CALCO.2025.14},
annote = {Keywords: parity game, compositionality, string diagram}
}
Document
(Co)algebraic pearl
Trees in Coalgebra from Generalized Reachability ((Co)algebraic pearl)
Abstract
An automaton is called reachable if every state is reachable from the initial state. This notion has been generalized coalgebraically in two ways: first, via a universal property on pointed coalgebras, namely, that a reachable coalgebra has no proper subcoalgebra; and second, a coalgebra is reachable if it arises as the union of an iterative computation of successor states, starting from the initial state.
In the current paper, we present corresponding universal properties and iterative constructions for trees. The universal property captures when a coalgebra is a tree, namely, when it has no proper tree unravelling. The iterative construction unravels an arbitrary coalgebra to a tree. We show that this yields the expected notion of tree for a variety of standard examples.
We obtain our characterization of trees by first generalizing the previous theory of reachable coalgebras. Surprisingly, both the universal property and the iterative construction for trees arise as an instance of this generalized notion of reachability.
Cite as
Thorsten Wißmann, Bálint Kocsis, Jurriaan Rot, and Ruben Turkenburg. Trees in Coalgebra from Generalized Reachability ((Co)algebraic pearl). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{wimann_et_al:LIPIcs.CALCO.2025.15,
author = {Wi{\ss}mann, Thorsten and Kocsis, B\'{a}lint and Rot, Jurriaan and Turkenburg, Ruben},
title = {{Trees in Coalgebra from Generalized Reachability}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.15},
URN = {urn:nbn:de:0030-drops-235740},
doi = {10.4230/LIPIcs.CALCO.2025.15},
annote = {Keywords: Trees, Coalgebra, Factorization Systems}
}
Document
(Co)algebraic pearl
Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl)
Abstract
We give a new proof of a result from well quasi-order theory on the computability of bases for upwards-closed sets of words. This new proof is based on Angluin’s L* algorithm, that learns an automaton from a minimally adequate teacher. This relates in particular two results from the 1980s: Angluin’s L* algorithm, and a result from Valk and Jantzen on the computability of bases for upwards-closed sets of tuples of integers.
Along the way, we describe an algorithm for learning quasi-ordered automata from a minimally adequate teacher, and extend a generalization of Valk and Jantzen’s result, encompassing both words and integers, to finitely generated monoids.
Cite as
Quentin Aristote. Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 16:1-16:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{aristote:LIPIcs.CALCO.2025.16,
author = {Aristote, Quentin},
title = {{Active Learning of Upward-Closed Sets of Words}},
booktitle = {11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
pages = {16:1--16:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-383-6},
ISSN = {1868-8969},
year = {2025},
volume = {342},
editor = {C\^{i}rstea, Corina and Knapp, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.16},
URN = {urn:nbn:de:0030-drops-235751},
doi = {10.4230/LIPIcs.CALCO.2025.16},
annote = {Keywords: active learning, well quasi-orders, Valk-Jantzen lemma, piecewise-testable languages, monoids}
}