Document

**Published in:** LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Directed topology augments the concept of a topological space with a notion of directed paths. This leads to a category of directed spaces, in which the morphisms are continuous maps respecting directed paths. Directed topology thereby enables an accurate representation of computation paths in concurrent systems that usually cannot be reversed.
Even though ideas from algebraic topology have analogues in directed topology, the directedness drastically changes how spaces can be characterised. For instance, while an important homotopy invariant of a topological space is its fundamental groupoid, for directed spaces this has to be replaced by the fundamental category because directed paths are not necessarily reversible.
In this paper, we present a Lean 4 formalisation of directed spaces and of a Van Kampen theorem for them, which allows the fundamental category of a directed space to be computed in terms of the fundamental categories of subspaces. Part of this formalisation is also a significant theory of directed spaces, directed homotopy theory and path coverings, which can serve as basis for future formalisations of directed topology. The formalisation in Lean can also be used in computer-assisted reasoning about the behaviour of concurrent systems that have been represented as directed spaces.

Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.ITP.2024.8, author = {Basold, Henning and Bruin, Peter and Lawson, Dominique}, title = {{The Directed Van Kampen Theorem in Lean}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8}, URN = {urn:nbn:de:0030-drops-207368}, doi = {10.4230/LIPIcs.ITP.2024.8}, annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics} }

Document

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

Causality appears in various contexts as a property where present behaviour can only depend on past events, but not on future events. In this paper, we compare three different notions of causality that capture the idea of causality in the form of restrictions on morphisms between coinductively defined structures, such as final coalgebras and chains, in fairly general categories. We then focus on one presentation and show that it gives rise to a traced symmetric monoidal category of causal morphisms. This shows that causal morphisms are closed under sequential and parallel composition and, crucially, under recursion.

Henning Basold and Tanjona Ralaivaosaona. Composition and Recursion for Causal Structures. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.CALCO.2023.18, author = {Basold, Henning and Ralaivaosaona, Tanjona}, title = {{Composition and Recursion for Causal Structures}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {18:1--18:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.18}, URN = {urn:nbn:de:0030-drops-188157}, doi = {10.4230/LIPIcs.CALCO.2023.18}, annote = {Keywords: Causal morphisms, Final Coalgebras, Final Chains, Metric Maps, Guarded Recursion, Traced Symmetric Monoidal Category} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

LIPIcs, Volume 239, TYPES 2021, Complete Volume

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{basold_et_al:LIPIcs.TYPES.2021, title = {{LIPIcs, Volume 239, TYPES 2021, Complete Volume}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {1--280}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021}, URN = {urn:nbn:de:0030-drops-167680}, doi = {10.4230/LIPIcs.TYPES.2021}, annote = {Keywords: LIPIcs, Volume 239, TYPES 2021, Complete Volume} }

Document

Front Matter

**Published in:** LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Front Matter, Table of Contents, Preface, Conference Organization

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.TYPES.2021.0, author = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {0:i--0:viii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.0}, URN = {urn:nbn:de:0030-drops-167691}, doi = {10.4230/LIPIcs.TYPES.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }

Document

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

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.

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.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

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

Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties.
Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.

Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.CALCO.2017.5, author = {Basold, Henning and Pous, Damien and Rot, Jurriaan}, title = {{Monoidal Company for Accessible Functors}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {5:1--5:16}, 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.5}, URN = {urn:nbn:de:0030-drops-80379}, doi = {10.4230/LIPIcs.CALCO.2017.5}, annote = {Keywords: coalgebras, distributive laws, accessible functors, monoidal categories} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail