23 Search Results for "Roggenbach, Markus"


Volume

LIPIcs, Volume 139

8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

CALCO 2019, June 3-6, 2019, London, United Kingdom

Editors: Markus Roggenbach and Ana Sokolova

Document
Complete Volume
LIPIcs, Volume 139, CALCO'19, Complete Volume

Authors: Markus Roggenbach and Ana Sokolova

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


Abstract
LIPIcs, Volume 139, CALCO'19, Complete Volume

Cite as

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


Copy BibTex To Clipboard

@Proceedings{roggenbach_et_al:LIPIcs.CALCO.2019,
  title =	{{LIPIcs, Volume 139, CALCO'19, Complete Volume}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019},
  URN =		{urn:nbn:de:0030-drops-115619},
  doi =		{10.4230/LIPIcs.CALCO.2019},
  annote =	{Keywords: Theory of computation, Models of computation; Modal and temporal logics; Algebraic semantics; Categorical semantics, Quantum computation theory; Software and its engineering, Specification languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Markus Roggenbach and Ana Sokolova

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


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

Cite as

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


Copy BibTex To Clipboard

@InProceedings{roggenbach_et_al:LIPIcs.CALCO.2019.0,
  author =	{Roggenbach, Markus and Sokolova, Ana},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{0:i--0:x},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.0},
  URN =		{urn:nbn:de:0030-drops-114282},
  doi =		{10.4230/LIPIcs.CALCO.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors: Xiaohong Chen and Grigore Roşu

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


Abstract
K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.

Cite as

Xiaohong Chen and Grigore Roşu. Matching mu-Logic: Foundation of K Framework (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
  author =	{Chen, Xiaohong and Ro\c{s}u, Grigore},
  title =	{{Matching mu-Logic: Foundation of K Framework}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{1:1--1:4},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
  URN =		{urn:nbn:de:0030-drops-114296},
  doi =		{10.4230/LIPIcs.CALCO.2019.1},
  annote =	{Keywords: Matching mu-logic, Program verification, Reachability logic}
}
Document
Invited Paper
From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper)

Authors: Stefan Milius

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


Abstract
This extended abstract first presents a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.

Cite as

Stefan Milius. From Equational Specifications of Algebras with Structure to Varieties of Data Languages (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{milius:LIPIcs.CALCO.2019.2,
  author =	{Milius, Stefan},
  title =	{{From Equational Specifications of Algebras with Structure to Varieties of Data Languages}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{2:1--2:5},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.2},
  URN =		{urn:nbn:de:0030-drops-114309},
  doi =		{10.4230/LIPIcs.CALCO.2019.2},
  annote =	{Keywords: Birkhoff theorem, Equational logic, Eilenberg theorem, Data languages}
}
Document
Invited Paper
Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper)

Authors: Mehrnoosh Sadrzadeh

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


Abstract
Residuated monoids model the structure of sentences. Vectors provide meaning representations for words. A functorial mapping between the two is obtained by lifting the vectors to tensors. The resulting sentence representations solve similarity, disambiguation and entailment tasks.

Cite as

Mehrnoosh Sadrzadeh. Principles of Natural Language, Logic, and Tensor Semantics (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 3:1-3:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sadrzadeh:LIPIcs.CALCO.2019.3,
  author =	{Sadrzadeh, Mehrnoosh},
  title =	{{Principles of Natural Language, Logic, and Tensor Semantics}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{3:1--3:4},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.3},
  URN =		{urn:nbn:de:0030-drops-114312},
  doi =		{10.4230/LIPIcs.CALCO.2019.3},
  annote =	{Keywords: Residuated Monoids, Vector Space Semantics, Corpora of Textual Data, Sentence Similarity and Disambiguation}
}
Document
Invited Paper
Coinduction: Automata, Formal Proof, Companions (Invited Paper)

Authors: Damien Pous

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


Abstract
Coinduction is a mathematical tool that is used pervasively in computer science: to program and reason about infinite data-structures, to give semantics to concurrent systems, to obtain automata algorithms. We present some of these applications in automata theory and in formalised mathematics. Then we discuss recent developments on the abstract theory of coinduction and its enhancements.

Cite as

Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{pous:LIPIcs.CALCO.2019.4,
  author =	{Pous, Damien},
  title =	{{Coinduction: Automata, Formal Proof, Companions}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{4:1--4:4},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.4},
  URN =		{urn:nbn:de:0030-drops-114323},
  doi =		{10.4230/LIPIcs.CALCO.2019.4},
  annote =	{Keywords: Coinduction, Automata, Coalgebra, Formal proofs}
}
Document
Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages

Authors: Vincenzo Ciancia and Yde Venema

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


Abstract
In this work, we provide a simple coalgebraic characterisation of regular omega-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Omega-automata. In earlier work we introduced Omega-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Omega-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Omega-automata are expressively complete for the regular omega-languages. We show that, due to their coalgebraic nature, Omega-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Omega-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular omega-languages.

Cite as

Vincenzo Ciancia and Yde Venema. Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{ciancia_et_al:LIPIcs.CALCO.2019.5,
  author =	{Ciancia, Vincenzo and Venema, Yde},
  title =	{{Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{5:1--5:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.5},
  URN =		{urn:nbn:de:0030-drops-114338},
  doi =		{10.4230/LIPIcs.CALCO.2019.5},
  annote =	{Keywords: omega-automata, regular omega-languages, coalgebra, streams, bisimilarity}
}
Document
Tree Automata as Algebras: Minimisation and Determinisation

Authors: Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva

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


Abstract
We study a categorical generalisation of tree automata, as algebras for a fixed endofunctor endowed with initial and final states. Under mild assumptions about the base category, we present a general minimisation algorithm for these automata. We then build upon and extend an existing generalisation of the Nerode equivalence to a categorical setting and relate it to the existence of minimal automata. Finally, we show that generalised types of side-effects, such as non-determinism, can be captured by this categorical framework, leading to a general determinisation procedure.

Cite as

Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree Automata as Algebras: Minimisation and Determinisation. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{vanheerdt_et_al:LIPIcs.CALCO.2019.6,
  author =	{van Heerdt, Gerco and Kapp\'{e}, Tobias and Rot, Jurriaan and Sammartino, Matteo and Silva, Alexandra},
  title =	{{Tree Automata as Algebras: Minimisation and Determinisation}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{6:1--6:22},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.6},
  URN =		{urn:nbn:de:0030-drops-114341},
  doi =		{10.4230/LIPIcs.CALCO.2019.6},
  annote =	{Keywords: tree automata, algebras, minimisation, determinisation, Nerode equivalence}
}
Document
Coalgebraic Geometric Logic

Authors: Nick Bezhanishvili, Jim de Groot, and Yde Venema

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


Abstract
Using the theory of coalgebra, we introduce a uniform framework for adding modalities to the language of propositional geometric logic. Models for this logic are based on coalgebras for an endofunctor T on some full subcategory of the category Top of topological spaces and continuous functions. We compare the notions of modal equivalence, behavioural equivalence and bisimulation on the resulting class of models, and we provide a final object for the corresponding category. Furthermore, we specify a method of lifting an endofunctor on Set, accompanied by a collection of predicate liftings, to an endofunctor on the category of topological spaces.

Cite as

Nick Bezhanishvili, Jim de Groot, and Yde Venema. Coalgebraic Geometric Logic. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bezhanishvili_et_al:LIPIcs.CALCO.2019.7,
  author =	{Bezhanishvili, Nick and de Groot, Jim and Venema, Yde},
  title =	{{Coalgebraic Geometric Logic}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{7:1--7:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.7},
  URN =		{urn:nbn:de:0030-drops-114354},
  doi =		{10.4230/LIPIcs.CALCO.2019.7},
  annote =	{Keywords: Coalgebra, Geometric Logic, Modal Logic, Topology}
}
Document
Coinduction in Flow: The Later Modality in Fibrations

Authors: Henning Basold

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


Abstract
This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search. Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.

Cite as

Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{basold:LIPIcs.CALCO.2019.8,
  author =	{Basold, Henning},
  title =	{{Coinduction in Flow: The Later Modality in Fibrations}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{8:1--8:22},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.8},
  URN =		{urn:nbn:de:0030-drops-114369},
  doi =		{10.4230/LIPIcs.CALCO.2019.8},
  annote =	{Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Up-to techniques, Probabilistic Logic, Probabilistic Programming}
}
Document
Causal Unfoldings

Authors: Marc de Visme and Glynn Winskel

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


Abstract
In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history.

Cite as

Marc de Visme and Glynn Winskel. Causal Unfoldings. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{devisme_et_al:LIPIcs.CALCO.2019.9,
  author =	{de Visme, Marc and Winskel, Glynn},
  title =	{{Causal Unfoldings}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{9:1--9:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.9},
  URN =		{urn:nbn:de:0030-drops-114376},
  doi =		{10.4230/LIPIcs.CALCO.2019.9},
  annote =	{Keywords: Event Structures, Parallel Causes, Causal Unfolding, Probability}
}
Document
A Coalgebraic Perspective on Probabilistic Logic Programming

Authors: Tao Gu and Fabio Zanasi

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


Abstract
Probabilistic logic programming is increasingly important in artificial intelligence and related fields as a formalism to reason about uncertainty. It generalises logic programming with the possibility of annotating clauses with probabilities. This paper proposes a coalgebraic perspective on probabilistic logic programming. Programs are modelled as coalgebras for a certain functor F, and two semantics are given in terms of cofree coalgebras. First, the cofree F-coalgebra yields a semantics in terms of derivation trees. Second, by embedding F into another type G, as cofree G-coalgebra we obtain a "possible worlds" interpretation of programs, from which one may recover the usual distribution semantics of probabilistic logic programming.

Cite as

Tao Gu and Fabio Zanasi. A Coalgebraic Perspective on Probabilistic Logic Programming. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gu_et_al:LIPIcs.CALCO.2019.10,
  author =	{Gu, Tao and Zanasi, Fabio},
  title =	{{A Coalgebraic Perspective on Probabilistic Logic Programming}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{10:1--10:21},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.10},
  URN =		{urn:nbn:de:0030-drops-114387},
  doi =		{10.4230/LIPIcs.CALCO.2019.10},
  annote =	{Keywords: probabilistic logic programming, coalgebraic semantics, distribution semantics}
}
Document
Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity

Authors: Astrid Belder, Bas Luttik, and Jos Baeten

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


Abstract
The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.

Cite as

Astrid Belder, Bas Luttik, and Jos Baeten. Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{belder_et_al:LIPIcs.CALCO.2019.11,
  author =	{Belder, Astrid and Luttik, Bas and Baeten, Jos},
  title =	{{Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{11:1--11:22},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.11},
  URN =		{urn:nbn:de:0030-drops-114390},
  doi =		{10.4230/LIPIcs.CALCO.2019.11},
  annote =	{Keywords: Sequencing, Sequential composition, Bisimilarity, Axiomatisation, Decidability}
}
Document
On Terminal Coalgebras Derived from Initial Algebras

Authors: Jiří Adámek

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


Abstract
A number of important set functors have countable initial algebras, but terminal coalgebras are uncountable or even non-existent. We prove that the countable cardinality is an anomaly: every set functor with an initial algebra of a finite or uncountable regular cardinality has a terminal coalgebra of the same cardinality. We also present a number of categories that are algebraically complete and cocomplete, i.e., every endofunctor has an initial algebra and a terminal coalgebra. Finally, for finitary set functors we prove that the initial algebra mu F and terminal coalgebra nu F carry a canonical ultrametric with the joint Cauchy completion. And the algebra structure of mu F determines, by extending its inverse continuously, the coalgebra structure of nu F.

Cite as

Jiří Adámek. On Terminal Coalgebras Derived from Initial Algebras. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{adamek:LIPIcs.CALCO.2019.12,
  author =	{Ad\'{a}mek, Ji\v{r}{\'\i}},
  title =	{{On Terminal Coalgebras Derived from Initial Algebras}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{12:1--12:21},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.12},
  URN =		{urn:nbn:de:0030-drops-114403},
  doi =		{10.4230/LIPIcs.CALCO.2019.12},
  annote =	{Keywords: terminal coalgebras, initial algebras, algebraically complete category, finitary functor, fixed points of functors}
}
  • Refine by Author
  • 2 Roggenbach, Markus
  • 2 Sobociński, Paweł
  • 2 Sokolova, Ana
  • 2 Venema, Yde
  • 2 Zanasi, Fabio
  • Show More...

  • Refine by Classification
  • 8 Theory of computation → Categorical semantics
  • 7 Theory of computation → Logic
  • 3 Software and its engineering → Specification languages
  • 3 Theory of computation → Algebraic semantics
  • 3 Theory of computation → Formal languages and automata theory
  • Show More...

  • Refine by Keyword
  • 2 Coalgebra
  • 2 Coinduction
  • 2 string diagrams
  • 1 Automata
  • 1 Axiom of choice
  • Show More...

  • Refine by Type
  • 22 document
  • 1 volume

  • Refine by Publication Year
  • 23 2019

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