Volume
LIPIcs, Volume 270
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Publication Details
- published at: 2023-09-02
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-287-7
- DBLP: db/conf/calco/calco2023
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 270, CALCO 2023, Complete Volume
Abstract
LIPIcs, Volume 270, CALCO 2023, Complete Volume
Cite as
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 1-336, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{baldan_et_al:LIPIcs.CALCO.2023,
title = {{LIPIcs, Volume 270, CALCO 2023, Complete Volume}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {1--336},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023},
URN = {urn:nbn:de:0030-drops-187967},
doi = {10.4230/LIPIcs.CALCO.2023},
annote = {Keywords: LIPIcs, Volume 270, CALCO 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CALCO.2023.0,
author = {Baldan, Paolo and de Paiva, Valeria},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.0},
URN = {urn:nbn:de:0030-drops-187976},
doi = {10.4230/LIPIcs.CALCO.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Integrating Cost and Behavior in Type Theory (Invited Talk)
Abstract
The computational view of intuitionistic dependent type theory is as an intrinsic logic of (functional) programs in which types are viewed as specifications of their behavior. Equational reasoning is particularly relevant in the functional case, where correctness can be formulated as equality between two implementations of the same behavior. Besides behavior, it is also important to specify and verify the cost of programs, measured in terms of their resource usage, with respect to both sequential and parallel evaluation. Although program cost can - and has been - verified in type theory using an extrinsic formulation of programs as data objects, what we seek here is, instead, an intrinsic account within type theory itself.
In this talk we discuss Calf, the Cost-Aware Logical Framework, which is an extension of dependent call-by-push-value type theory that provides an intrinsic account of both parallel and sequential resource usage for a variety of problem-specific measures of cost. Thus, for example, it is possible to prove that insertion sort and merge sort are equal as regards behavior, but differ in terms of the number of comparisons required to achieve the same results. But how can equal functions have different cost? To provide an intrinsic account of both intensional and extensional properties of programs, we make use of Sterling’s notion of Synthetic Tait Computability, a generalization of Tait’s method originally developed for the study of higher type theory.
In STC the concept of a "phase" plays a central role: originally as the distinction between the syntactic and semantic aspects of a computability structure, but more recently applied to the formulation of type theories for program modules and for information flow properties of programs. In Calf we distinguish two phases, the intensional and extensional, which differ as regards the significance of cost accounting - extensionally it is neglected, intensionally it is of paramount importance. Thus, in the extensional phase insertion sort and merge sort are equal, but in the intensional phase they are distinct, and indeed one is proved to have optimal behavior as regards comparisons, and the other not. Importantly, both phases are needed in a cost verification - the proof of the complexity of an algorithm usually relies on aspects of its correctness.
We will provide an overview of Calf itself, and of its application in the verification of the cost and behavior of a variety of programs. So far we have been able to verify cost bounds on Euclid’s Algorithm, amortized bounds on batched queues, parallel cost bounds on a joinable form of red-black trees, and the equivalence and cost of the aforementioned sorting methods. In a companion paper at this meeting Grodin and I develop an account of amortization that relates the standard inductive view of instruction seequences with the coinductive view of data structures characterized by the same operations. In ongoing work we are extending the base of verified deterministic algorithms to those taught in the undergraduate parallel algorithms course at Carnegie Mellon, and are extending Calf itself to account for probabilistic methods, which are also used in that course.
(This talk represents joint work with Yue Niu, Harrison Grodin, and Jon Sterling.)
Cite as
Robert Harper. Integrating Cost and Behavior in Type Theory (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{harper:LIPIcs.CALCO.2023.1,
author = {Harper, Robert},
title = {{Integrating Cost and Behavior in Type Theory}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.1},
URN = {urn:nbn:de:0030-drops-187980},
doi = {10.4230/LIPIcs.CALCO.2023.1},
annote = {Keywords: type theory, analysis of algorithms, program verification}
}
Document
Invited Talk
Local Completeness for Program Correctness and Incorrectness (Invited Talk)
Abstract
Program correctness techniques aim to prove the absence of bugs, but can yield false alarms because they tend to over-approximate program semantics. Vice versa, program incorrectness methods are aimed to detect true bugs, without false alarms, but cannot be used to prove correctness, because they under-approximate program semantics. In this invited talk we will overview our ongoing research on the use of the abstract interpretation framework to combine under- and over-approximation in the same analysis and distill a logic for program correctness and incorrectness.
Cite as
Roberto Bruni. Local Completeness for Program Correctness and Incorrectness (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bruni:LIPIcs.CALCO.2023.2,
author = {Bruni, Roberto},
title = {{Local Completeness for Program Correctness and Incorrectness}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.2},
URN = {urn:nbn:de:0030-drops-187993},
doi = {10.4230/LIPIcs.CALCO.2023.2},
annote = {Keywords: Program analysis, program verification, Hoare logic, incorrectness logic, abstract interpretation, local completeness}
}
Document
Invited Talk
A Tour on Ecumenical Systems (Invited Talk)
Abstract
Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully. In this paper, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz' seminal work [Dag Prawitz, 2015]. We will begin by elucidating Prawitz' concept of "ecumenism" and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics. We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.
Cite as
Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3,
author = {Pimentel, Elaine and Pereira, Luiz Carlos},
title = {{A Tour on Ecumenical Systems}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {3:1--3:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3},
URN = {urn:nbn:de:0030-drops-188003},
doi = {10.4230/LIPIcs.CALCO.2023.3},
annote = {Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory}
}
Document
Invited Talk
The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk)
Abstract
Gradually typed languages offer both static and dynamic checking of program invariants, from simple properties such as type safety, to more advanced ones such as information flow control (security), relational parametricity (theorems for free), and program correctness. To ensure that gradually typed languages behave as expected, researchers prove theorems about their language designs. For example, the Gradual Guarantee Theorem states that a programmer can migrate their program to become more or less statically checked and the resulting program will behave the same (modulo errors). As another example, the Noninterference Theorem (for information flow control) states that high security inputs do not affect the low security outputs of a program. These theorems are often proved using simulation arguments or via syntactic logical relations and modal logics. Sometimes the proofs are mechanized in a proof assistant, but often they are simply written in LaTeX. However, as researchers consider gradual languages of growing complexity, the time to conduct such proofs, and/or the likelihood of errors in the proofs, also grows. As a result there is a need for improved proof techniques and libraries of mechanized results that would help to streamline the development of the metatheory of gradually typed languages.
Cite as
Jeremy G. Siek. The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{siek:LIPIcs.CALCO.2023.4,
author = {Siek, Jeremy G.},
title = {{The Metatheory of Gradual Typing: State of the Art and Challenges}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {4:1--4:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.4},
URN = {urn:nbn:de:0030-drops-188019},
doi = {10.4230/LIPIcs.CALCO.2023.4},
annote = {Keywords: gradual typing, type safety, gradual guarantee, noninterference, simulation, logical relation, mechanized metatheory}
}
Document
Invited Talk
Machine-Checked Computational Mathematics (Invited Talk)
Abstract
This talk shall discuss the potential impact of formal methods, and in particular, of interactive theorem proving, on computational mathematics.
Geared with increasingly fast computer algebra libraries and scientific computing software, computers have become amazing instruments for mathematical guesswork. In fact, computer calculations are even sometimes used to substantiate actual reasoning steps in proofs, later published in major venues of the mathematical literature. Yet surprisingly, little of the now standard techniques available today for verifying critical software (e.g., cryptographic components, airborne commands, etc.) have been applied to the programs used to produce mathematics. In this talk, we propose to discuss this state of affairs.
Cite as
Assia Mahboubi. Machine-Checked Computational Mathematics (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mahboubi:LIPIcs.CALCO.2023.5,
author = {Mahboubi, Assia},
title = {{Machine-Checked Computational Mathematics}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {5:1--5:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.5},
URN = {urn:nbn:de:0030-drops-188024},
doi = {10.4230/LIPIcs.CALCO.2023.5},
annote = {Keywords: Type theory, computer algebra, interactive theorem proving}
}
Document
Forward and Backward Steps in a Fibration
Abstract
Distributive laws of various kinds occur widely in the theory of coalgebra, for instance to model automata constructions and trace semantics, and to interpret coalgebraic modal logic. We study steps, which are a general type of distributive law, that allow one to map coalgebras along an adjunction. In this paper, we address the question of what such mappings do to well known notions of equivalence, e.g., bisimilarity, behavioural equivalence, and logical equivalence.
We do this using the characterisation of such notions of equivalence as (co)inductive predicates in a fibration. Our main contribution is the identification of conditions on the interaction between the steps and liftings, which guarantees preservation of fixed points by the mapping of coalgebras along the adjunction. We apply these conditions in the context of lax liftings proposed by Bonchi, Silva, Sokolova (2021), and generalise their result on preservation of bisimilarity in the construction of a belief state transformer. Further, we relate our results to properties of coalgebraic modal logics including expressivity and completeness.
Cite as
Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot. Forward and Backward Steps in a Fibration. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{turkenburg_et_al:LIPIcs.CALCO.2023.6,
author = {Turkenburg, Ruben and Beohar, Harsh and Kupke, Clemens and Rot, Jurriaan},
title = {{Forward and Backward Steps in a Fibration}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.6},
URN = {urn:nbn:de:0030-drops-188032},
doi = {10.4230/LIPIcs.CALCO.2023.6},
annote = {Keywords: Coalgebra, Fibration, Bisimilarity}
}
Document
Structural Operational Semantics for Heterogeneously Typed Coalgebras
Abstract
Concurrently interacting components of a modular software architecture are heterogeneously structured behavioural models. We consider them as coalgebras based on different endofunctors. We formalize the composition of these coalgebras as specially tailored segments of distributive laws of the bialgebraic approach of Turi and Plotkin. The resulting categorical rules for structural operational semantics involve many-sorted algebraic specifications, which leads to a description of the components together with the composed system as a single holistic behavioural system. We evaluate our approach by showing that observational equivalence is a congruence with respect to the algebraic composition operation.
Cite as
Harald König, Uwe Wolter, and Tim Kräuter. Structural Operational Semantics for Heterogeneously Typed Coalgebras. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{konig_et_al:LIPIcs.CALCO.2023.7,
author = {K\"{o}nig, Harald and Wolter, Uwe and Kr\"{a}uter, Tim},
title = {{Structural Operational Semantics for Heterogeneously Typed Coalgebras}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.7},
URN = {urn:nbn:de:0030-drops-188048},
doi = {10.4230/LIPIcs.CALCO.2023.7},
annote = {Keywords: Coalgebra, Bialgebra, Structural operational semantics, Compositionality}
}
Document
Interpolation Is (Not Always) Easy to Spoil
Abstract
We study a version of the Craig interpolation theorem as formulated in the framework of the theory of institutions. This formulation proved crucial in the development of a number of key results concerning foundations of software specification and formal development. We investigate preservation of interpolation under extensions of institutions by new models and sentences. We point out that some interpolation properties remain stable under such extensions, even if quite arbitrary new models or sentences are permitted. We give complete characterisations of such situations for institution extensions by new models, by new sentences, as well as by new models and sentences, respectively.
Cite as
Andrzej Tarlecki. Interpolation Is (Not Always) Easy to Spoil. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{tarlecki:LIPIcs.CALCO.2023.8,
author = {Tarlecki, Andrzej},
title = {{Interpolation Is (Not Always) Easy to Spoil}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {8:1--8:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.8},
URN = {urn:nbn:de:0030-drops-188059},
doi = {10.4230/LIPIcs.CALCO.2023.8},
annote = {Keywords: interpolation, institutions, institutional abstract model theory, specification theory}
}
Document
String Diagram Rewriting Modulo Commutative (Co)Monoid Structure
Abstract
String diagrams constitute an intuitive and expressive graphical syntax that has found application in a very diverse range of fields including concurrency theory, quantum computing, control theory, machine learning, linguistics, and digital circuits. Rewriting theory for string diagrams relies on a combinatorial interpretation as double-pushout rewriting of certain hypergraphs. As previously studied, there is a "tension" in this interpretation: in order to make it sound and complete, we either need to add structure on string diagrams (in particular, Frobenius algebra structure) or pose restrictions on double-pushout rewriting (resulting in "convex" rewriting). From the string diagram viewpoint, imposing a full Frobenius structure may not always be natural or desirable in applications, which motivates our study of a weaker requirement: commutative monoid structure. In this work we characterise string diagram rewriting modulo commutative monoid equations, via a sound and complete interpretation in a suitable notion of double-pushout rewriting of hypergraphs.
Cite as
Aleksandar Milosavljević, Robin Piedeleu, and Fabio Zanasi. String Diagram Rewriting Modulo Commutative (Co)Monoid Structure. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{milosavljevic_et_al:LIPIcs.CALCO.2023.9,
author = {Milosavljevi\'{c}, Aleksandar and Piedeleu, Robin and Zanasi, Fabio},
title = {{String Diagram Rewriting Modulo Commutative (Co)Monoid Structure}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.9},
URN = {urn:nbn:de:0030-drops-188067},
doi = {10.4230/LIPIcs.CALCO.2023.9},
annote = {Keywords: String diagrams, Double-pushout rewriting, Commutative monoid}
}
Document
Strongly Finitary Monads for Varieties of Quantitative Algebras
Abstract
Quantitative algebras are algebras enriched in the category Met of metric spaces or UMet of ultrametric spaces so that all operations are nonexpanding. Mardare, Plotkin and Panangaden introduced varieties (aka 1-basic varieties) as classes of quantitative algebras presented by quantitative equations. We prove that, when restricted to ultrametrics, varieties bijectively correspond to strongly finitary monads T on UMet. This means that T is the left Kan extension of its restriction to finite discrete spaces. An analogous result holds in the category CUMet of complete ultrametric spaces.
Cite as
Jiří Adámek, Matěj Dostál, and Jiří Velebil. Strongly Finitary Monads for Varieties of Quantitative Algebras. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2023.10,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Dost\'{a}l, Mat\v{e}j and Velebil, Ji\v{r}{\'\i}},
title = {{Strongly Finitary Monads for Varieties of Quantitative Algebras}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {10:1--10:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.10},
URN = {urn:nbn:de:0030-drops-188078},
doi = {10.4230/LIPIcs.CALCO.2023.10},
annote = {Keywords: quantitative algebras, ultra-quantitative algebras, strongly finitary monads, varieties}
}
Document
Generators and Bases for Monadic Closures
Abstract
It is well-known that every regular language admits a unique minimal deterministic acceptor. Establishing an analogous result for non-deterministic acceptors is significantly more difficult, but nonetheless of great practical importance. To tackle this issue, a number of sub-classes of non-deterministic automata have been identified, all admitting canonical minimal representatives. In previous work, we have shown that such representatives can be recovered categorically in two steps. First, one constructs the minimal bialgebra accepting a given regular language, by closing the minimal coalgebra with additional algebraic structure over a monad. Second, one identifies canonical generators for the algebraic part of the bialgebra, to derive an equivalent coalgebra with side effects in a monad. In this paper, we further develop the general theory underlying these two steps. On the one hand, we show that deriving a minimal bialgebra from a minimal coalgebra can be realized by applying a monad on an appropriate category of subobjects. On the other hand, we explore the abstract theory of generators and bases for algebras over a monad.
Cite as
Stefan Zetzsche, Alexandra Silva, and Matteo Sammartino. Generators and Bases for Monadic Closures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{zetzsche_et_al:LIPIcs.CALCO.2023.11,
author = {Zetzsche, Stefan and Silva, Alexandra and Sammartino, Matteo},
title = {{Generators and Bases for Monadic Closures}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.11},
URN = {urn:nbn:de:0030-drops-188084},
doi = {10.4230/LIPIcs.CALCO.2023.11},
annote = {Keywords: Monads, Category Theory, Generators, Automata, Coalgebras, Bialgebras}
}
Document
Bisimilar States in Uncertain Structures
Abstract
We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. We remedy the lack of sufficiency by a characterization of uncertain bisimilarity in terms of coalgebraic simulations.
Cite as
Jurriaan Rot and Thorsten Wißmann. Bisimilar States in Uncertain Structures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{rot_et_al:LIPIcs.CALCO.2023.12,
author = {Rot, Jurriaan and Wi{\ss}mann, Thorsten},
title = {{Bisimilar States in Uncertain Structures}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {12:1--12:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.12},
URN = {urn:nbn:de:0030-drops-188094},
doi = {10.4230/LIPIcs.CALCO.2023.12},
annote = {Keywords: Coalgebra, Relation Lifting, Bisimilarity, Mealy Machines, ioco}
}
Document
A Category for Unifying Gaussian Probability and Nondeterminism
Abstract
We introduce categories of extended Gaussian maps and Gaussian relations which unify Gaussian probability distributions with relational nondeterminism in the form of linear relations. Both have crucial and well-understood applications in statistics, engineering, and control theory, but combining them in a single formalism is challenging. It enables us to rigorously describe a variety of phenomena like noisy physical laws, Willems' theory of open systems and uninformative priors in Bayesian statistics. The core idea is to formally admit vector subspaces D ⊆ X as generalized uniform probability distribution. Our formalism represents a first bridge between the literature on categorical systems theory (signal-flow diagrams, linear relations, hypergraph categories) and notions of probability theory.
Cite as
Dario Stein and Richard Samuelson. A Category for Unifying Gaussian Probability and Nondeterminism. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{stein_et_al:LIPIcs.CALCO.2023.13,
author = {Stein, Dario and Samuelson, Richard},
title = {{A Category for Unifying Gaussian Probability and Nondeterminism}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.13},
URN = {urn:nbn:de:0030-drops-188107},
doi = {10.4230/LIPIcs.CALCO.2023.13},
annote = {Keywords: systems theory, hypergraph categories, Bayesian inference, category theory, Markov categories}
}
Document
Fractals from Regular Behaviours
Abstract
We are interested in connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner’s expressions for processes as contraction operators on a complete metric space. When the space is, for example, the plane, the denotations of fixed point terms correspond to familiar fractal sets. We give a sound and complete axiomatization of fractal equivalence, the congruence on terms consisting of pairs that construct identical self-similar sets in all interpretations. We further make connections to labelled Markov chains and to invariant measures. In all of this work, we use important results from process calculi. For example, we use Rabinovich’s completeness theorem for trace equivalence in our own completeness theorem. In addition to our results, we also raise many questions related to both fractals and process calculi.
Cite as
Todd Schmid, Victoria Noquez, and Lawrence S. Moss. Fractals from Regular Behaviours. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{schmid_et_al:LIPIcs.CALCO.2023.14,
author = {Schmid, Todd and Noquez, Victoria and Moss, Lawrence S.},
title = {{Fractals from Regular Behaviours}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.14},
URN = {urn:nbn:de:0030-drops-188111},
doi = {10.4230/LIPIcs.CALCO.2023.14},
annote = {Keywords: fixed-point terms, labelled transition system, fractal, final coalgebra, equational logic, completeness}
}
Document
Coinductive Control of Inductive Data Types
Abstract
We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.
Cite as
Paige Randall North and Maximilien Péroux. Coinductive Control of Inductive Data Types. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{north_et_al:LIPIcs.CALCO.2023.15,
author = {North, Paige Randall and P\'{e}roux, Maximilien},
title = {{Coinductive Control of Inductive Data Types}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.15},
URN = {urn:nbn:de:0030-drops-188129},
doi = {10.4230/LIPIcs.CALCO.2023.15},
annote = {Keywords: Inductive types, enriched category theory, algebraic data types, algebra, coalgebra}
}
Document
Weakly Markov Categories and Weakly Affine Monads
Abstract
Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal categories where each object is equipped with the structure of a commutative comonoid. They arise for example as Kleisli categories of commutative monads on cartesian categories, and as such they provide a general framework for effectful computation. Recently proposed in the context of categorical probability, Markov categories are gs-monoidal categories where the monoidal unit is also terminal, and they arise for example as Kleisli categories of commutative affine monads, where affine means that the monad preserves the monoidal unit.
The aim of this paper is to study a new condition on the gs-monoidal structure, resulting in the concept of weakly Markov categories, which is intermediate between gs-monoidal categories and Markov ones. In a weakly Markov category, the morphisms to the monoidal unit are not necessarily unique, but form a group. As we show, these categories exhibit a rich theory of conditional independence for morphisms, generalising the known theory for Markov categories. We also introduce the corresponding notion for commutative monads, which we call weakly affine, and for which we give two equivalent characterisations.
The paper argues that these monads are relevant to the study of categorical probability. A case at hand is the monad of finite non-zero measures, which is weakly affine but not affine. Such structures allow to investigate probability without normalisation within an elegant categorical framework.
Cite as
Tobias Fritz, Fabio Gadducci, Paolo Perrone, and Davide Trotta. Weakly Markov Categories and Weakly Affine Monads. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fritz_et_al:LIPIcs.CALCO.2023.16,
author = {Fritz, Tobias and Gadducci, Fabio and Perrone, Paolo and Trotta, Davide},
title = {{Weakly Markov Categories and Weakly Affine Monads}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.16},
URN = {urn:nbn:de:0030-drops-188133},
doi = {10.4230/LIPIcs.CALCO.2023.16},
annote = {Keywords: String diagrams, gs-monoidal and Markov categories, categorical probability, affine monads}
}
Document
Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties
Abstract
We study many-valued coalgebraic logics with primal algebras of truth-degrees. We describe a way to lift algebraic semantics of classical coalgebraic logics, given by an endofunctor on the variety of Boolean algebras, to this many-valued setting, and we show that many important properties of the original logic are inherited by its lifting. Then, we deal with the problem of obtaining a concrete axiomatic presentation of the variety of algebras for this lifted logic, given that we know one for the original one. We solve this problem for a class of presentations which behaves well with respect to a lattice structure on the algebra of truth-degrees.
Cite as
Alexander Kurz and Wolfgang Poiger. Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kurz_et_al:LIPIcs.CALCO.2023.17,
author = {Kurz, Alexander and Poiger, Wolfgang},
title = {{Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.17},
URN = {urn:nbn:de:0030-drops-188147},
doi = {10.4230/LIPIcs.CALCO.2023.17},
annote = {Keywords: coalgebraic modal logic, many-valued logic, primal algebras, algebraic semantics, presenting functors}
}
Document
Composition and Recursion for Causal Structures
Abstract
Causality appears in various contexts as a property where present behaviour can only depend on past events, but not on future events. In this paper, we compare three different notions of causality that capture the idea of causality in the form of restrictions on morphisms between coinductively defined structures, such as final coalgebras and chains, in fairly general categories. We then focus on one presentation and show that it gives rise to a traced symmetric monoidal category of causal morphisms. This shows that causal morphisms are closed under sequential and parallel composition and, crucially, under recursion.
Cite as
Henning Basold and Tanjona Ralaivaosaona. Composition and Recursion for Causal Structures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{basold_et_al:LIPIcs.CALCO.2023.18,
author = {Basold, Henning and Ralaivaosaona, Tanjona},
title = {{Composition and Recursion for Causal Structures}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.18},
URN = {urn:nbn:de:0030-drops-188157},
doi = {10.4230/LIPIcs.CALCO.2023.18},
annote = {Keywords: Causal morphisms, Final Coalgebras, Final Chains, Metric Maps, Guarded Recursion, Traced Symmetric Monoidal Category}
}
Document
Aczel-Mendler Bisimulations in a Regular Category
Abstract
Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of axiom of choice, so that the theory enjoys desirable properties, such as closure under composition. In this paper, we accommodate the definition in a general regular category - which does not necessarily satisfy any form of axiom of choice. We show that this general definition 1) is closed under composition without using the axiom of choice, 2) coincides with other types of coalgebraic formulations under milder conditions, 3) coincides with the usual definition when the category has the regular axiom of choice. We then develop the particular case of toposes, where the formulation becomes nicer thanks to the power-object monad, and extend the formalism to simulations. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.
Cite as
Jérémy Dubut. Aczel-Mendler Bisimulations in a Regular Category. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dubut:LIPIcs.CALCO.2023.19,
author = {Dubut, J\'{e}r\'{e}my},
title = {{Aczel-Mendler Bisimulations in a Regular Category}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.19},
URN = {urn:nbn:de:0030-drops-188163},
doi = {10.4230/LIPIcs.CALCO.2023.19},
annote = {Keywords: Regular Categories, Toposes, Bisimulations, Coalgebra}
}
Document
(Co)algebraic pearls
Completeness for Categories of Generalized Automata ((Co)algebraic pearls)
Abstract
We present a slick proof of completeness and cocompleteness for categories of F-automata, where the span of maps E ←d E⊗ I s→ O that usually defines a deterministic automaton of input I and output O in a monoidal category (K,⊗) is replaced by a span E ← FE → O for a generic endofunctor F : K → K of a generic category K: these automata exist in their "Mealy" and "Moore" version and form categories F-Mly and F-Mre; such categories can be presented as strict 2-pullbacks in Cat and whenever F is a left adjoint, both F-Mly and F-Mre admit all limits and colimits that K admits. We mechanize our main results using the proof assistant Agda and the library https://github.com/agda/agda-categories.
Cite as
Guido Boccali, Andrea Laretto, Fosco Loregian, and Stefano Luneia. Completeness for Categories of Generalized Automata ((Co)algebraic pearls). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 20:1-20:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{boccali_et_al:LIPIcs.CALCO.2023.20,
author = {Boccali, Guido and Laretto, Andrea and Loregian, Fosco and Luneia, Stefano},
title = {{Completeness for Categories of Generalized Automata}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {20:1--20:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.20},
URN = {urn:nbn:de:0030-drops-188174},
doi = {10.4230/LIPIcs.CALCO.2023.20},
annote = {Keywords: Deterministic automata, Moore machines, Mealy machines, coalgebras, cocomplete category}
}
Document
(Co)algebraic pearls
On Kripke, Vietoris and Hausdorff Polynomial Functors ((Co)algebraic pearls)
Abstract
The Vietoris space of compact subsets of a given Hausdorff space yields an endofunctor V on the category of Hausdorff spaces. Vietoris polynomial endofunctors on that category are built from V, the identity and constant functors by forming products, coproducts and compositions. These functors are known to have terminal coalgebras and we deduce that they also have initial algebras. We present an analogous class of endofunctors on the category of extended metric spaces, using in lieu of V the Hausdorff functor ℋ. We prove that the ensuing Hausdorff polynomial functors have terminal coalgebras and initial algebras. Whereas the canonical constructions of terminal coalgebras for Vietoris polynomial functors takes ω steps, one needs ω + ω steps in general for Hausdorff ones. We also give a new proof that the closed set functor on metric spaces has no fixed points.
Cite as
Jiří Adámek, Stefan Milius, and Lawrence S. Moss. On Kripke, Vietoris and Hausdorff Polynomial Functors ((Co)algebraic pearls). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2023.21,
author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.},
title = {{On Kripke, Vietoris and Hausdorff Polynomial Functors}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {21:1--21:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.21},
URN = {urn:nbn:de:0030-drops-188189},
doi = {10.4230/LIPIcs.CALCO.2023.21},
annote = {Keywords: Hausdorff functor, Vietoris functor, initial algebra, terminal coalgebra}
}
Document
Early Ideas
CRDTs, Coalgebraically (Early Ideas)
Abstract
We describe ongoing work that models conflict-free replicated data types (CRDTs) from a coalgebraic point of view. CRDTs are data structures designed for replication across multiple physical locations in a distributed system. We show how to model a CRDT at the local replica level using a novel coalgebraic semantics for CRDTs. We believe this is the first step towards presenting a unified theory for specifying and verifying CRDTs and replicated state machines. As a case study, we consider emulation of CRDTs in terms of coalgebra.
Cite as
Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, and Lindsey Kuper. CRDTs, Coalgebraically (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{liittschwager_et_al:LIPIcs.CALCO.2023.22,
author = {Liittschwager, Nathan and Tsampas, Stelios and Castello, Jonathan and Kuper, Lindsey},
title = {{CRDTs, Coalgebraically}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {22:1--22:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.22},
URN = {urn:nbn:de:0030-drops-188198},
doi = {10.4230/LIPIcs.CALCO.2023.22},
annote = {Keywords: Coalgebra, Distributed Systems, Concurrency, Bisimulation}
}
Document
Early Ideas
Amortized Analysis via Coinduction (Early Ideas)
Abstract
Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in calf, a dependent type theory for cost analysis.
Cite as
Harrison Grodin and Robert Harper. Amortized Analysis via Coinduction (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{grodin_et_al:LIPIcs.CALCO.2023.23,
author = {Grodin, Harrison and Harper, Robert},
title = {{Amortized Analysis via Coinduction}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {23:1--23:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.23},
URN = {urn:nbn:de:0030-drops-188201},
doi = {10.4230/LIPIcs.CALCO.2023.23},
annote = {Keywords: amortized analysis, coinduction, data structure, mechanized proof}
}
Document
Early Ideas
Higher-Order Mathematical Operational Semantics (Early Ideas)
Abstract
We present a higher-order extension of Turi and Plotkin’s abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe’s method is developed. It encompasses, for instance, Abramsky’s classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.
Cite as
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Higher-Order Mathematical Operational Semantics (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 24:1-24:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{goncharov_et_al:LIPIcs.CALCO.2023.24,
author = {Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
title = {{Higher-Order Mathematical Operational Semantics}},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
pages = {24:1--24:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-287-7},
ISSN = {1868-8969},
year = {2023},
volume = {270},
editor = {Baldan, Paolo and de Paiva, Valeria},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.24},
URN = {urn:nbn:de:0030-drops-188213},
doi = {10.4230/LIPIcs.CALCO.2023.24},
annote = {Keywords: Abstract GSOS, lambda-calculus, applicative bisimilarity, bialgebra}
}