7 Search Results for "Dubois, Catherine"

Document
DOI: 10.4230/LIPIcs.STACS.2026.6
Threshold-Driven Streaming Graph: Expansion and Rumor Spreading

Authors: Flora Angileri, Andrea Clementi, Emanuele Natale, Michele Salvi, and Isabella Ziccardi

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
A randomized distributed algorithm called RAES was introduced in [Becchetti et al., 2020] to extract a bounded-degree expander from a dense n-vertex expander graph G = (V, E). The algorithm relies on a simple threshold-based procedure. A key assumption in [Becchetti et al., 2020] is that the input graph G is static - i.e., both its vertex set V and edge set E remain unchanged throughout the process - while the analysis of raes in dynamic models is left as a major open question. In this work, we investigate the behavior of RAES under a dynamic graph model induced by a streaming node-churn process (also known as the sliding window model), where, at each discrete round, a new node joins the graph and the oldest node departs. This process yields a bounded-degree dynamic graph 𝒢 = {G_t = (V_t, E_t) : t ∈ ℕ} that captures essential characteristics of peer-to-peer networks - specifically, node churn and threshold on the number of connections each node can manage. We prove that every snapshot G_t in the dynamic graph sequence has good expansion properties with high probability. Furthermore, we leverage this property to establish a logarithmic upper bound on the completion time of the well-known PUSH and PULL rumor spreading protocols over the dynamic graph 𝒢.
Cite as

Flora Angileri, Andrea Clementi, Emanuele Natale, Michele Salvi, and Isabella Ziccardi. Threshold-Driven Streaming Graph: Expansion and Rumor Spreading. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{angileri_et_al:LIPIcs.STACS.2026.6,
  author =	{Angileri, Flora and Clementi, Andrea and Natale, Emanuele and Salvi, Michele and Ziccardi, Isabella},
  title =	{{Threshold-Driven Streaming Graph: Expansion and Rumor Spreading}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.6},
  URN =		{urn:nbn:de:0030-drops-254957},
  doi =		{10.4230/LIPIcs.STACS.2026.6},
  annote =	{Keywords: Distributed Algorithms, Randomized Algorithms, Dynamic Random Graphs, Graph Expansion, Rumor Spreading}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.39
A Canonical Form for Universe Levels in Impredicative Type Theory

Authors: Yoan Géran

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.
Cite as

Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{geran:LIPIcs.CSL.2026.39,
  author =	{G\'{e}ran, Yoan},
  title =	{{A Canonical Form for Universe Levels in Impredicative Type Theory}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.39},
  URN =		{urn:nbn:de:0030-drops-254640},
  doi =		{10.4230/LIPIcs.CSL.2026.39},
  annote =	{Keywords: universe levels, canonical form, impredicativity, imax algebra}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.7
An Operational Semantics in Isabelle/HOL-CSP

Authors: Benoît Ballenghien and Burkhart Wolff

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

Abstract
The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today a reference model for concurrency. In the fairly rich literature, several versions of operational semantics have been discussed, which should be consistent with the denotational one. This work is based on Isabelle/HOL-CSP 2.0, a shallow embedding of the failure-divergence model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties. In several ways, HOL-CSP is actually an extension of the original setting in the sense that it admits higher-order processes and infinite alphabets. In this paper, we present a construction and formal equivalence proofs between operational CSP semantics and the underlying denotational failure-divergence semantics. The construction is based on a definition of the operational transition operator P ⇝e P’ basically via the After operator and the classical failure-divergence refinement. Several choices are discussed to formally derive the operational semantics leading to subtle differences. The derived operational semantics for symbolic Labelled Transition Systems (LTSs) can be potentially used for certifications of model-checker logs as well as combined proof techniques.
Cite as

Benoît Ballenghien and Burkhart Wolff. An Operational Semantics in Isabelle/HOL-CSP. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ballenghien_et_al:LIPIcs.ITP.2024.7,
  author =	{Ballenghien, Beno\^{i}t and Wolff, Burkhart},
  title =	{{An Operational Semantics in Isabelle/HOL-CSP}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{7:1--7: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.7},
  URN =		{urn:nbn:de:0030-drops-207355},
  doi =		{10.4230/LIPIcs.ITP.2024.7},
  annote =	{Keywords: Process-Algebra, Semantics, Concurrency, Computational Models, Theorem Proving, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.11
Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families

Authors: Catherine Dubois, Nicolas Magaud, and Alain Giorgetti

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are very compact ones and usually rely on the use of dependent types, but they tend to be difficult to handle in practice. On the contrary, implementations based on a larger (and simpler) data structure combined with a restriction property are much easier to deal with. In this work, we study several families related to lambda terms, among which Motzkin trees, seen as lambda term skeletons, closable Motzkin trees, corresponding to closed lambda terms, and a parameterized family of open lambda terms. For each of these families, we define two different representations, show that they are isomorphic and provide tools to switch from one representation to another. All these datatypes and their associated transformations are implemented in the Coq proof assistant. Furthermore we implement random generators for each representation, using the QuickChick plugin.
Cite as

Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dubois_et_al:LIPIcs.TYPES.2022.11,
  author =	{Dubois, Catherine and Magaud, Nicolas and Giorgetti, Alain},
  title =	{{Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.11},
  URN =		{urn:nbn:de:0030-drops-184548},
  doi =		{10.4230/LIPIcs.TYPES.2022.11},
  annote =	{Keywords: Data Representations, Isomorphisms, dependent Types, formal Proofs, random Generation, lambda Terms, Coq}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.12
A Semantics of 𝕂 into Dedukti

Authors: Amélie Ledein, Valentin Blot, and Catherine Dubois

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore. Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions. In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.
Cite as

Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12,
  author =	{Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine},
  title =	{{A Semantics of \mathbb{K} into Dedukti}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.12},
  URN =		{urn:nbn:de:0030-drops-184557},
  doi =		{10.4230/LIPIcs.TYPES.2022.12},
  annote =	{Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory}
}
Document
DOI: 10.4230/DagRep.6.10.75
Universality of Proofs (Dagstuhl Seminar 16421)

Authors: Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe

Published in: Dagstuhl Reports, Volume 6, Issue 10 (2017)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16421 "Universality of Proofs" which took place October 16-21, 2016. The seminar was motivated by the fact that it is nowadays difficult to exchange proofs from one proof assistant to another one. Thus a formal proof cannot be considered as a universal proof, reusable in different contexts. The seminar aims at providing a comprehensive overview of the existing techniques for interoperability and going further into the development of a common objective and framework for proof developments that support the communication, reuse and interoperability of proofs. The seminar included participants coming from different fields of computer science such as logic, proof engineering, program verification, formal mathematics. It included overview talks, technical talks and breakout sessions. This report collects the abstracts of talks and summarizes the outcomes of the breakout sessions.
Cite as

Gilles Dowek, Catherine Dubois, Brigitte Pientka, and Florian Rabe. Universality of Proofs (Dagstuhl Seminar 16421). In Dagstuhl Reports, Volume 6, Issue 10, pp. 75-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{dowek_et_al:DagRep.6.10.75,
  author =	{Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian},
  title =	{{Universality of Proofs (Dagstuhl Seminar 16421)}},
  pages =	{75--98},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{10},
  editor =	{Dowek, Gilles and Dubois, Catherine and Pientka, Brigitte and Rabe, Florian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.10.75},
  URN =		{urn:nbn:de:0030-drops-69514},
  doi =		{10.4230/DagRep.6.10.75},
  annote =	{Keywords: Formal proofs, Interoperability, Logical frameworks, Logics, Proof formats, Provers, Reusability}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.47
Objects and Subtyping in the Lambda-Pi-Calculus Modulo

Authors: Raphaël Cauderlier and Catherine Dubois

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo.
Cite as

Raphaël Cauderlier and Catherine Dubois. Objects and Subtyping in the Lambda-Pi-Calculus Modulo. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 47-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cauderlier_et_al:LIPIcs.TYPES.2014.47,
  author =	{Cauderlier, Rapha\"{e}l and Dubois, Catherine},
  title =	{{Objects and Subtyping in the Lambda-Pi-Calculus Modulo}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{47--71},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.47},
  URN =		{urn:nbn:de:0030-drops-54919},
  doi =		{10.4230/LIPIcs.TYPES.2014.47},
  annote =	{Keywords: object, calculus, encoding, dependent type, rewrite system}
}
  • Refine by Type
  • 7 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 1 2024
  • 2 2023
  • 1 2017
  • 1 2015

  • Refine by Author
  • 4 Dubois, Catherine
  • 1 Angileri, Flora
  • 1 Ballenghien, Benoît
  • 1 Blot, Valentin
  • 1 Cauderlier, Raphaël
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 DagRep

  • Refine by Classification
  • 2 Theory of computation → Type theory
  • 1 General and reference → Verification
  • 1 Theory of computation → Design and analysis of algorithms
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Higher order logic
  • Show More...

  • Refine by Keyword
  • 2 Semantics
  • 1 Computational Models
  • 1 Concurrency
  • 1 Coq
  • 1 Data Representations
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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