Search Results

Documents authored by Dubut, Jérémy

Document
DOI: 10.4230/LIPIcs.CALCO.2023.19
Aczel-Mendler Bisimulations in a Regular Category

Authors: Jérémy Dubut

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

Abstract
Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of axiom of choice, so that the theory enjoys desirable properties, such as closure under composition. In this paper, we accommodate the definition in a general regular category - which does not necessarily satisfy any form of axiom of choice. We show that this general definition 1) is closed under composition without using the axiom of choice, 2) coincides with other types of coalgebraic formulations under milder conditions, 3) coincides with the usual definition when the category has the regular axiom of choice. We then develop the particular case of toposes, where the formulation becomes nicer thanks to the power-object monad, and extend the formalism to simulations. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.
Cite as

Jérémy Dubut. Aczel-Mendler Bisimulations in a Regular Category. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dubut:LIPIcs.CALCO.2023.19,
  author =	{Dubut, J\'{e}r\'{e}my},
  title =	{{Aczel-Mendler Bisimulations in a Regular Category}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.19},
  URN =		{urn:nbn:de:0030-drops-188163},
  doi =		{10.4230/LIPIcs.CALCO.2023.19},
  annote =	{Keywords: Regular Categories, Toposes, Bisimulations, Coalgebra}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.34
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)

Authors: Akihisa Yamada and Jérémy Dubut

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL’s ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.
Cite as

Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.34},
  URN =		{urn:nbn:de:0030-drops-184092},
  doi =		{10.4230/LIPIcs.ITP.2023.34},
  annote =	{Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.30
Complete Non-Orders and Fixed Points

Authors: Akihisa Yamada and Jérémy Dubut

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
Cite as

Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2019.30,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Complete Non-Orders and Fixed Points}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.30},
  URN =		{urn:nbn:de:0030-drops-110852},
  doi =		{10.4230/LIPIcs.ITP.2019.30},
  annote =	{Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.9
The Directed Homotopy Hypothesis

Authors: Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be "equivalent" to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.
Cite as

Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. The Directed Homotopy Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dubut_et_al:LIPIcs.CSL.2016.9,
  author =	{Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
  title =	{{The Directed Homotopy Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.9},
  URN =		{urn:nbn:de:0030-drops-65492},
  doi =		{10.4230/LIPIcs.CSL.2016.9},
  annote =	{Keywords: directed algebraic topology, partially enriched categories, homotopy hypothesis, geometric models for concurrency, higher category theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.25
Bisimulations and Unfolding in P-Accessible Categorical Models

Authors: Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In this paper, we propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueing of paths. We prove that transitions systems and pre sheaf models are a particular case of our framework. We also prove that in our framework, several characterizations of bisimulation coincide, in particular an "operational one" akin to the standard definition in transition systems. Also, accessibility is preserved by coreflexions. We then design a notion of unfolding, which has good properties in the accessible case: its is a right adjoint and is a universal covering, i.e., initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, coincides with an unfolding, when the category of path shapes is well chosen.
Cite as

Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Bisimulations and Unfolding in P-Accessible Categorical Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dubut_et_al:LIPIcs.CONCUR.2016.25,
  author =	{Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
  title =	{{Bisimulations and Unfolding in P-Accessible Categorical Models}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{25:1--25:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.25},
  URN =		{urn:nbn:de:0030-drops-61555},
  doi =		{10.4230/LIPIcs.CONCUR.2016.25},
  annote =	{Keywords: categorical models, bisimulation, coreflexions, unfolding, universal covering}
}
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