36 Search Results for "Baldan, Paolo"

Volume

LIPIcs, Volume 270

10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA

Editors: Paolo Baldan and Valeria de Paiva

Document
Complete Volume
DOI: 10.4230/LIPIcs.CALCO.2023
LIPIcs, Volume 270, CALCO 2023, Complete Volume

Authors: Paolo Baldan and Valeria de Paiva

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Paolo Baldan and Valeria de Paiva

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.1
Integrating Cost and Behavior in Type Theory (Invited Talk)

Authors: Robert Harper

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.2
Local Completeness for Program Correctness and Incorrectness (Invited Talk)

Authors: Roberto Bruni

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.4
The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk)

Authors: Jeremy G. Siek

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.5
Machine-Checked Computational Mathematics (Invited Talk)

Authors: Assia Mahboubi

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.6
Forward and Backward Steps in a Fibration

Authors: Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.7
Structural Operational Semantics for Heterogeneously Typed Coalgebras

Authors: Harald König, Uwe Wolter, and Tim Kräuter

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.8
Interpolation Is (Not Always) Easy to Spoil

Authors: Andrzej Tarlecki

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.9
String Diagram Rewriting Modulo Commutative (Co)Monoid Structure

Authors: Aleksandar Milosavljević, Robin Piedeleu, and Fabio Zanasi

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.10
Strongly Finitary Monads for Varieties of Quantitative Algebras

Authors: Jiří Adámek, Matěj Dostál, and Jiří Velebil

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.11
Generators and Bases for Monadic Closures

Authors: Stefan Zetzsche, Alexandra Silva, and Matteo Sammartino

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.12
Bisimilar States in Uncertain Structures

Authors: Jurriaan Rot and Thorsten Wißmann

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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
DOI: 10.4230/LIPIcs.CALCO.2023.13
A Category for Unifying Gaussian Probability and Nondeterminism

Authors: Dario Stein and Richard Samuelson

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.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}
}
  • Refine by Author
  • 10 Baldan, Paolo
  • 6 König, Barbara
  • 3 Padoan, Tommaso
  • 2 Adámek, Jiří
  • 2 Bonchi, Filippo
  • Show More...

  • Refine by Classification
  • 9 Theory of computation → Categorical semantics
  • 7 Theory of computation → Logic and verification
  • 5 Theory of computation → Modal and temporal logics
  • 5 Theory of computation → Models of computation
  • 4 Theory of computation → Algebraic semantics
  • Show More...

  • Refine by Keyword
  • 5 Coalgebra
  • 3 coalgebra
  • 2 Bisimilarity
  • 2 Event structures
  • 2 String diagrams
  • Show More...

  • Refine by Type
  • 35 document
  • 1 volume

  • Refine by Publication Year
  • 28 2023
  • 2 2020
  • 2 2021
  • 1 2005
  • 1 2014
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact