Search Results

Documents authored by Bonchi, Filippo

Document
DOI: 10.4230/LIPIcs.MFCS.2024.30
When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines

Authors: Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere’s hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.
Cite as

Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.MFCS.2024.30,
  author =	{Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide},
  title =	{{When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.30},
  URN =		{urn:nbn:de:0030-drops-205867},
  doi =		{10.4230/LIPIcs.MFCS.2024.30},
  annote =	{Keywords: relational algebra, hyperdoctrines, cartesian bicategories, string diagrams}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.40
Diagrammatic Polyhedral Algebra

Authors: Filippo Bonchi, Alessandro Di Giorgio, and Paweł Sobociński

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
We extend the theory of Interacting Hopf algebras with an order primitive, and give a sound and complete axiomatisation of the prop of polyhedral cones. Next, we axiomatise an affine extension and prove soundness and completeness for the prop of polyhedra.
Cite as

Filippo Bonchi, Alessandro Di Giorgio, and Paweł Sobociński. Diagrammatic Polyhedral Algebra. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.FSTTCS.2021.40,
  author =	{Bonchi, Filippo and Di Giorgio, Alessandro and Soboci\'{n}ski, Pawe{\l}},
  title =	{{Diagrammatic Polyhedral Algebra}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.40},
  URN =		{urn:nbn:de:0030-drops-155511},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.40},
  annote =	{Keywords: String diagrams, Polyhedral cones, Polyhedra}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.9
From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls)

Authors: Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
Farkas' lemma is a celebrated result on the solutions of systems of linear inequalities, which finds application pervasively in mathematics and computer science. In this work we show how to formulate and prove Farkas' lemma in diagrammatic polyhedral algebra, a sound and complete graphical calculus for polyhedra. Furthermore, we show how linear programs can be modeled within the calculus and how some famous duality results can be proved.
Cite as

Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi. From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.9,
  author =	{Bonchi, Filippo and Di Giorgio, Alessandro and Zanasi, Fabio},
  title =	{{From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9},
  URN =		{urn:nbn:de:0030-drops-153643},
  doi =		{10.4230/LIPIcs.CALCO.2021.9},
  annote =	{Keywords: String diagrams, Farkas Lemma, Duality, Linear Programming}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2021.10
On Doctrines and Cartesian Bicategories

Authors: Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We study the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.
Cite as

Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10,
  author =	{Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
  title =	{{On Doctrines and Cartesian Bicategories}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10},
  URN =		{urn:nbn:de:0030-drops-153656},
  doi =		{10.4230/LIPIcs.CALCO.2021.10},
  annote =	{Keywords: Cartesian bicategories, elementary existential doctrines, string diagram}
}
Document
(Co)algebraic pearls
DOI: 10.4230/LIPIcs.CALCO.2021.11
Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls)

Authors: Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions.
Cite as

Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11,
  author =	{Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria},
  title =	{{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11},
  URN =		{urn:nbn:de:0030-drops-153666},
  doi =		{10.4230/LIPIcs.CALCO.2021.11},
  annote =	{Keywords: Convex sets of distributions monad, Convex semilattices, Unique base}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.MFCS.2021
LIPIcs, Volume 202, MFCS 2021, Complete Volume

Authors: Filippo Bonchi and Simon J. Puglisi

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
LIPIcs, Volume 202, MFCS 2021, Complete Volume
Cite as

46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 1-1560, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{bonchi_et_al:LIPIcs.MFCS.2021,
  title =	{{LIPIcs, Volume 202, MFCS 2021, Complete Volume}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{1--1560},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021},
  URN =		{urn:nbn:de:0030-drops-144396},
  doi =		{10.4230/LIPIcs.MFCS.2021},
  annote =	{Keywords: LIPIcs, Volume 202, MFCS 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.MFCS.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Filippo Bonchi and Simon J. Puglisi

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.MFCS.2021.0,
  author =	{Bonchi, Filippo and Puglisi, Simon J.},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.0},
  URN =		{urn:nbn:de:0030-drops-144409},
  doi =		{10.4230/LIPIcs.MFCS.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.15
The Axiom of Choice in Cartesian Bicategories

Authors: Filippo Bonchi, Jens Seeber, and Paweł Sobociński

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.
Cite as

Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2019.15,
  author =	{Bonchi, Filippo and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}},
  title =	{{The Axiom of Choice in Cartesian Bicategories}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.15},
  URN =		{urn:nbn:de:0030-drops-114439},
  doi =		{10.4230/LIPIcs.CALCO.2019.15},
  annote =	{Keywords: Cartesian bicategories, Axiom of choice, string diagrams}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.37
Bialgebraic Semantics for String Diagrams

Authors: Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Turi and Plotkin’s bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law for that monad. As a proof of concept, we provide bialgebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, à la Hoare and à la Milner.
Cite as

Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Bialgebraic Semantics for String Diagrams. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2019.37,
  author =	{Bonchi, Filippo and Piedeleu, Robin and Sobocinski, Pawel and Zanasi, Fabio},
  title =	{{Bialgebraic Semantics for String Diagrams}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.37},
  URN =		{urn:nbn:de:0030-drops-109398},
  doi =		{10.4230/LIPIcs.CONCUR.2019.37},
  annote =	{Keywords: String Diagram, Structural Operational Semantics, Bialgebraic semantics}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.17
Up-To Techniques for Behavioural Metrics via Fibrations

Authors: Filippo Bonchi, Barbara König, and Daniela Petrisan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.
Cite as

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17,
  author =	{Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela},
  title =	{{Up-To Techniques for Behavioural Metrics via Fibrations}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17},
  URN =		{urn:nbn:de:0030-drops-95552},
  doi =		{10.4230/LIPIcs.CONCUR.2018.17},
  annote =	{Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.13
Graphical Conjunctive Queries

Authors: Filippo Bonchi, Jens Seeber, and Pawel Sobocinski

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The Calculus of Conjunctive Queries (CCQ) has foundational status in database theory. A celebrated theorem of Chandra and Merlin states that CCQ query inclusion is decidable. Its proof transforms logical formulas to graphs: each query has a natural model - a kind of graph - and query inclusion reduces to the existence of a graph homomorphism between natural models. We introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as CCQ. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters' notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin's insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.
Cite as

Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2018.13,
  author =	{Bonchi, Filippo and Seeber, Jens and Sobocinski, Pawel},
  title =	{{Graphical Conjunctive Queries}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{13:1--13:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.13},
  URN =		{urn:nbn:de:0030-drops-96805},
  doi =		{10.4230/LIPIcs.CSL.2018.13},
  annote =	{Keywords: conjunctive query inclusion, string diagrams, cartesian bicategories}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CALCO.2017
LIPIcs, Volume 72, CALCO'17, Complete Volume

Authors: Filippo Bonchi and Barbara König

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
LIPIcs, Volume 72, CALCO'17, Complete Volume
Cite as

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{bonchi_et_al:LIPIcs.CALCO.2017,
  title =	{{LIPIcs, Volume 72, CALCO'17, Complete Volume}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017},
  URN =		{urn:nbn:de:0030-drops-82059},
  doi =		{10.4230/LIPIcs.CALCO.2017},
  annote =	{Keywords: Theory of Computation, Models of computation, Logics and Meanings of Programs, Semantics of Programming Languages – Algebraic Approach}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CALCO.2017.0
Front Matter, Table of Contents, Preface, List of Authors

Authors: Filippo Bonchi and Barbara König

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
Front Matter, Table of Contents, Preface, List of Authors
Cite as

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2017.0,
  author =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  title =	{{Front Matter, Table of Contents, Preface, List of Authors}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.0},
  URN =		{urn:nbn:de:0030-drops-80284},
  doi =		{10.4230/LIPIcs.CALCO.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, List of Authors}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.23
The Power of Convex Algebras

Authors: Filippo Bonchi, Alexandra Silva, and Ana Sokolova

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Probabilistic automata (PA) combine probability and nondeterminism. They can be given different semantics, like strong bisimilarity, convex bisimilarity, or (more recently) distribution bisimilarity. The latter is based on the view of PA as transformers of probability distributions, also called belief states, and promotes distributions to first-class citizens. We give a coalgebraic account of the latter semantics, and explain the genesis of the belief-state transformer from a PA. To do so, we make explicit the convex algebraic structure present in PA and identify belief-state transformers as transition systems with state space that carries a convex algebra. As a consequence of our abstract approach, we can give a sound proof technique which we call bisimulation up-to convex hull.
Cite as

Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.23,
  author =	{Bonchi, Filippo and Silva, Alexandra and Sokolova, Ana},
  title =	{{The Power of Convex Algebras}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.23},
  URN =		{urn:nbn:de:0030-drops-77966},
  doi =		{10.4230/LIPIcs.CONCUR.2017.23},
  annote =	{Keywords: belief-state transformers, bisimulation up-to, coalgebra, convex algebra, convex powerset monad, probabilistic automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.24
Refinement for Signal Flow Graphs

Authors: Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
The symmetric monoidal theory of Interacting Hopf Algebras provides a sound and complete axiomatisation for linear relations over a given field. As is the case for ordinary relations, linear relations have a natural order that coincides with inclusion. In this paper, we give a presentation for this ordering by extending the theory of Interacting Hopf Algebras with a single additional inequation. We show that the extended theory gives rise to an abelian bicategory—a concept due to Carboni and Walters—and highlight similarities with the algebra of relations. Most importantly, the ordering leads to a well-behaved notion of refinement for signal flow graphs.
Cite as

Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski. Refinement for Signal Flow Graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.24,
  author =	{Bonchi, Filippo and Holland, Joshua and Pavlovic, Dusko and Sobocinski, Pawel},
  title =	{{Refinement for Signal Flow Graphs}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.24},
  URN =		{urn:nbn:de:0030-drops-77758},
  doi =		{10.4230/LIPIcs.CONCUR.2017.24},
  annote =	{Keywords: Signal flow graphs, refinement, operational semantics, string diagrams, symmetric monoidal inequality theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.35
Towards Trace Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.
Cite as

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards Trace Metrics via Functor Lifting. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 35-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CALCO.2015.35,
  author =	{Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
  title =	{{Towards Trace Metrics via Functor Lifting}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{35--49},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.35},
  URN =		{urn:nbn:de:0030-drops-55254},
  doi =		{10.4230/LIPIcs.CALCO.2015.35},
  annote =	{Keywords: trace metric, monad lifting, pseudometric, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.240
Lax Bialgebras and Up-To Techniques for Weak Bisimulations

Authors: Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.
Cite as

Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2015.240,
  author =	{Bonchi, Filippo and Petrisan, Daniela and Pous, Damien and Rot, Jurriaan},
  title =	{{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{240--253},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.240},
  URN =		{urn:nbn:de:0030-drops-53709},
  doi =		{10.4230/LIPIcs.CONCUR.2015.240},
  annote =	{Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.403
Behavioral Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha : X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor /F in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final /F-coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha : X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent.
Cite as

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 403-415, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.FSTTCS.2014.403,
  author =	{Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
  title =	{{Behavioral Metrics via Functor Lifting}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{403--415},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.403},
  URN =		{urn:nbn:de:0030-drops-48599},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.403},
  annote =	{Keywords: behavioral metric, functor lifting, pseudometric, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.272
Generalizing the powerset construction, coalgebraically

Authors: Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor $F$ determines both the type of systems ($F$-coalgebras) and a notion of behavioral equivalence ($\sim_F$) amongst them. Many types of transition systems and their equivalences can be captured by a functor $F$. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.
Cite as

Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing the powerset construction, coalgebraically. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 272-283, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.FSTTCS.2010.272,
  author =	{Silva, Alexandra and Bonchi, Filippo and Bonsangue, Marcello M. and Rutten, Jan J. M. M.},
  title =	{{Generalizing the powerset construction, coalgebraically}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{272--283},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.272},
  URN =		{urn:nbn:de:0030-drops-28706},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.272},
  annote =	{Keywords: coalgebra, language equivalence, bisimilarity, powerset construction}
}
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact