14 Search Results for "Rahli, Vincent"

Document
DOI: 10.4230/LIPIcs.OPODIS.2025.7
Mobile Byzantine Agreement in a Trusted World

Authors: Bo Pan and Maria Potop-Butucaru

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
In this paper, we address the Byzantine Agreement problem in synchronous systems where Byzantine agents can move from process to process, corrupting their host. We focus on two representative models: Garay’s and Buhrman’s models. In Garay’s model, when a process has been left by the Byzantine agent, it enters a cured state, is aware of its condition, and can remain silent for a round to prevent the dissemination of incorrect information. In Buhrman’s model, a Byzantine agent moves together with the message. It has been shown that solving Byzantine Agreement requires at least 4t + 1 processes in Garay’s model, and at least 3t + 1 in Buhrman’s model. In this paper, we aim to increase the tolerance to mobile Byzantine agents by integrating a trusted counter abstraction into both models. This abstraction prevents nodes from equivocating. In the new models, we prove that at least 3t+1, respectively 2t+1 processors are needed to tolerate t mobile Byzantine agents. Furthermore, we propose novel Mobile Byzantine Agreement algorithms that match these new lower bounds for both Garay’s and Buhrman’s models, achieving agreement in 𝒪(n) synchronous rounds.
Cite as

Bo Pan and Maria Potop-Butucaru. Mobile Byzantine Agreement in a Trusted World. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pan_et_al:LIPIcs.OPODIS.2025.7,
  author =	{Pan, Bo and Potop-Butucaru, Maria},
  title =	{{Mobile Byzantine Agreement in a Trusted World}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.7},
  URN =		{urn:nbn:de:0030-drops-251809},
  doi =		{10.4230/LIPIcs.OPODIS.2025.7},
  annote =	{Keywords: Byzantine Agreement, Mobile Faults, Trusted Abstractions}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2025.12
Efficient Byzantine Reliable Broadcast in the Failure Case

Authors: Thomas Locher

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
Reliable broadcast is a fundamental primitive in distributed computing that is widely used in various applications. Several new reliable broadcast algorithms have been presented in recent years, primarily focusing on reducing the communication complexity, which is the total number of exchanged bits in the worst case. While significant progress has been achieved, all proposed algorithms share a common weakness. Executions may fail, i.e., no message is ever delivered, while incurring a communication complexity equal or nearly equal to the communication complexity of executions where a message is delivered. In fact, a single Byzantine node, acting as the dedicated sender, is sufficient to trigger such executions, causing all nodes to consume bandwidth in vain. This paper introduces the novel concept of a reliable broadcast detector, a distributed algorithm that can be coupled with a reliable broadcast algorithm to minimize the communication complexity of failed executions. Two concrete detectors are presented with different requirements and properties. Additionally, reliable broadcast algorithms that utilize detectors are introduced, the main algorithm guaranteeing an overhead factor, compared to an ideal failure-free execution, that tends to 2 as the network size increases. Furthermore, a lower bound is proven that an overhead factor of 5/3 is inevitable when the sender initially broadcasts the message, as is the case for the proposed algorithm. Therefore, it achieves a bound that is close to optimal for any algorithm with this property.
Cite as

Thomas Locher. Efficient Byzantine Reliable Broadcast in the Failure Case. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{locher:LIPIcs.OPODIS.2025.12,
  author =	{Locher, Thomas},
  title =	{{Efficient Byzantine Reliable Broadcast in the Failure Case}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.12},
  URN =		{urn:nbn:de:0030-drops-251854},
  doi =		{10.4230/LIPIcs.OPODIS.2025.12},
  annote =	{Keywords: asynchronous networks, reliable broadcast, communication complexity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.9
A Zoo of Continuity Properties in Constructive Type Theory

Authors: Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.
Cite as

Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baillon_et_al:LIPIcs.FSCD.2025.9,
  author =	{Baillon, Martin and Forster, Yannick and Mahboubi, Assia and P\'{e}drot, Pierre-Marie and Piquerez, Matthieu},
  title =	{{A Zoo of Continuity Properties in Constructive Type Theory}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.9},
  URN =		{urn:nbn:de:0030-drops-236245},
  doi =		{10.4230/LIPIcs.FSCD.2025.9},
  annote =	{Keywords: type theory, constructive mathematics, continuity, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.19
Internal Effectful Forcing in System T

Authors: Martín H. Escardó, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι ⇒ ι) ⇒ ι in the set-theoretical model is a continuous function (ℕ → ℕ) → ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.
Cite as

Martín H. Escardó, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Internal Effectful Forcing in System T. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{escardo_et_al:LIPIcs.FSCD.2025.19,
  author =	{Escard\'{o}, Mart{\'\i}n H. and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk},
  title =	{{Internal Effectful Forcing in System T}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.19},
  URN =		{urn:nbn:de:0030-drops-236344},
  doi =		{10.4230/LIPIcs.FSCD.2025.19},
  annote =	{Keywords: Effectful forcing, Continuity, System T, Constructive Mathematics}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.1
Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Authors: Liron Cohen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.
Cite as

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.FSCD.2025.1,
  author =	{Cohen, Liron},
  title =	{{Computation First: Rebuilding Constructivism with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.1},
  URN =		{urn:nbn:de:0030-drops-236167},
  doi =		{10.4230/LIPIcs.FSCD.2025.1},
  annote =	{Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.14
Near-Optimal Communication Byzantine Reliable Broadcast Under a Message Adversary

Authors: Timothé Albouy, Davide Frey, Ran Gelles, Carmit Hazay, Michel Raynal, Elad Michael Schiller, François Taïani, and Vassilis Zikas

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
We address the problem of Reliable Broadcast in asynchronous message-passing systems with n nodes, of which up to t are malicious (faulty), in addition to a message adversary that can drop some of the messages sent by correct (non-faulty) nodes. We present a Message-Adversary-Tolerant Byzantine Reliable Broadcast (MBRB) algorithm that communicates O(|m|+nκ) bits per node, where |m| represents the length of the application message and κ = Ω(log n) is a security parameter. This communication complexity is optimal up to the parameter κ. This significantly improves upon the state-of-the-art MBRB solution (Albouy, Frey, Raynal, and Taïani, TCS 2023), which incurs communication of O(n|m|+n²κ) bits per node. Our solution sends at most 4n² messages overall, which is asymptotically optimal. Reduced communication is achieved by employing coding techniques that replace the need for all nodes to (re-)broadcast the entire application message m. Instead, nodes forward authenticated fragments of the encoding of m using an erasure-correcting code. Under the cryptographic assumptions of threshold signatures and vector commitments, and assuming n > 3t+2d, where the adversary drops at most d messages per broadcast, our algorithm allows at least 𝓁 = n - t - (1 + ε)d (for any arbitrarily low ε > 0) correct nodes to reconstruct m, despite missing fragments caused by the malicious nodes and the message adversary.
Cite as

Timothé Albouy, Davide Frey, Ran Gelles, Carmit Hazay, Michel Raynal, Elad Michael Schiller, François Taïani, and Vassilis Zikas. Near-Optimal Communication Byzantine Reliable Broadcast Under a Message Adversary. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 14:1-14:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{albouy_et_al:LIPIcs.OPODIS.2024.14,
  author =	{Albouy, Timoth\'{e} and Frey, Davide and Gelles, Ran and Hazay, Carmit and Raynal, Michel and Schiller, Elad Michael and Ta\"{i}ani, Fran\c{c}ois and Zikas, Vassilis},
  title =	{{Near-Optimal Communication Byzantine Reliable Broadcast Under a Message Adversary}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{14:1--14:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.14},
  URN =		{urn:nbn:de:0030-drops-225503},
  doi =		{10.4230/LIPIcs.OPODIS.2024.14},
  annote =	{Keywords: Asynchronous message-passing, Byzantine fault-tolerance, Message adversary, Reliable broadcast, Erasure-correction codes, \{Threshold\} signatures, \{Vector commitments\}}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.16
Byzantine Reliable Broadcast with Low Communication and Time Complexity

Authors: Thomas Locher

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
Byzantine reliable broadcast is a fundamental problem in distributed computing, which has been studied extensively over the past decades. State-of-the-art algorithms are predominantly based on the approach to share encoded fragments of the broadcast message, yielding an asymptotically optimal communication complexity when the message size exceeds the network size, a condition frequently encountered in practice. However, algorithms following the standard coding approach incur an overhead factor of at least 3, which can already be a burden for bandwidth-constrained applications. Minimizing this overhead is an important objective with immediate benefits to protocols that use a reliable broadcast routine as a building block. This paper introduces a novel mechanism to lower the communication and computational complexity. Two algorithms are presented that employ this mechanism to reliably broadcast messages in an asynchronous network where less than a third of all nodes are Byzantine. The first algorithm reduces the overhead factor to 2 and has a time complexity of 3 if the sender is honest, whereas the second algorithm attains an optimal time complexity of 2 with the same overhead factor in the absence of equivocation. Moreover, an optimization is proposed that reduces the overhead factor to 3/2 under normal operation in practice. Lastly, a lower bound is proved that an overhead factor lower than 3/2 cannot be achieved for a relevant class of reliable broadcast algorithms.
Cite as

Thomas Locher. Byzantine Reliable Broadcast with Low Communication and Time Complexity. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{locher:LIPIcs.OPODIS.2024.16,
  author =	{Locher, Thomas},
  title =	{{Byzantine Reliable Broadcast with Low Communication and Time Complexity}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.16},
  URN =		{urn:nbn:de:0030-drops-225524},
  doi =		{10.4230/LIPIcs.OPODIS.2024.16},
  annote =	{Keywords: Asynchronous Networks, Reliable Broadcast, Communication Complexity}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.20
How Robust Are Synchronous Consensus Protocols?

Authors: Nenad Milošević, Daniel Cason, Zarko Milošević, and Fernando Pedone

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
Synchronous Byzantine fault-tolerant (BFT) protocols have long been a reality in an academic setting, yet their practicality remains debated. The main concern of skeptics of synchronous systems is that the correctness of these protocols depends on the timely delivery of all messages within a predefined synchronous bound, Δ. This dependency creates a challenging tradeoff between protocol correctness and performance, as Δ directly impacts both. In this paper, we examine this tradeoff in detail. Specifically, we introduce BoundBFT, a new synchronous BFT consensus protocol. We analyze how BoundBFT’s correctness can be compromised and use this analysis to design and implement the most effective attack strategies that malicious processes could employ. Furthermore, we experimentally determine the synchronous bound Δ that provides sufficient confidence in maintaining protocol correctness even in the presence of malicious replicas. Finally, we apply this discovered bound to BoundBFT, evaluate its performance, and compare it to state-of-the-art synchronous and partially synchronous protocols.
Cite as

Nenad Milošević, Daniel Cason, Zarko Milošević, and Fernando Pedone. How Robust Are Synchronous Consensus Protocols?. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 20:1-20:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{milosevic_et_al:LIPIcs.OPODIS.2024.20,
  author =	{Milo\v{s}evi\'{c}, Nenad and Cason, Daniel and Milo\v{s}evi\'{c}, Zarko and Pedone, Fernando},
  title =	{{How Robust Are Synchronous Consensus Protocols?}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{20:1--20:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.20},
  URN =		{urn:nbn:de:0030-drops-225560},
  doi =		{10.4230/LIPIcs.OPODIS.2024.20},
  annote =	{Keywords: Synchronous Consensus, Byzantine Failures, Blockchain}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2024.25
Reliable Communication in Hybrid Authentication and Trust Models

Authors: Rowdy Chotkan, Bart Cox, Vincent Rahli, and Jérémie Decouchant

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
Reliable communication is a fundamental distributed communication abstraction that allows any two nodes within a network to communicate with each other. It is necessary for more powerful communication primitives, such as broadcast and consensus. Using different authentication models, two classical protocols implement reliable communication in unknown and sufficiently connected networks. In the former, network links are authenticated, and processes rely on dissemination paths to authenticate messages. In the latter, processes generate digital signatures that are flooded throughout the network. This work considers the hybrid system model that combines authenticated links and authenticated processes. Additionally, we aim to leverage the possible presence of trusted nodes (e.g., network gateways) and trusted components (e.g., Intel SGX enclaves). We first extend the two classical reliable communication protocols to leverage trusted nodes. Then we propose DualRC, our most generic algorithm that considers the hybrid authentication model by manipulating dissemination paths and digital signatures, and leverages the possible presence of trusted nodes and trusted components. We describe and prove methods that establish whether our algorithms implement reliable communication on a given network.
Cite as

Rowdy Chotkan, Bart Cox, Vincent Rahli, and Jérémie Decouchant. Reliable Communication in Hybrid Authentication and Trust Models. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 25:1-25:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chotkan_et_al:LIPIcs.OPODIS.2024.25,
  author =	{Chotkan, Rowdy and Cox, Bart and Rahli, Vincent and Decouchant, J\'{e}r\'{e}mie},
  title =	{{Reliable Communication in Hybrid Authentication and Trust Models}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{25:1--25:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.25},
  URN =		{urn:nbn:de:0030-drops-225611},
  doi =		{10.4230/LIPIcs.OPODIS.2024.25},
  annote =	{Keywords: Reliable communication, Byzantine, Authentication models, Trust}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.37
Inductive Continuity via Brouwer Trees

Authors: Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, another formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of this "inductive" continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this formulation of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that this inductive continuity principle implies other forms of continuity principles.
Cite as

Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.MFCS.2023.37,
  author =	{Cohen, Liron and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk},
  title =	{{Inductive Continuity via Brouwer Trees}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.37},
  URN =		{urn:nbn:de:0030-drops-185718},
  doi =		{10.4230/LIPIcs.MFCS.2023.37},
  annote =	{Keywords: Continuity, Dialogue trees, Stateful computations, Intuitionistic Logic, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.15
Realizing Continuity Using Stateful Computations

Authors: Liron Cohen and Vincent Rahli

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. This paper presents a class of intuitionistic theories that features stateful computations, such as reference cells, and shows that these theories can be extended with continuity axioms. The modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled in the theory.
Cite as

Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.CSL.2023.15,
  author =	{Cohen, Liron and Rahli, Vincent},
  title =	{{Realizing Continuity Using Stateful Computations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.15},
  URN =		{urn:nbn:de:0030-drops-174761},
  doi =		{10.4230/LIPIcs.CSL.2023.15},
  annote =	{Keywords: Continuity, Stateful computations, Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda}
}
Document
DOI: 10.4230/LITES.8.2.2
Swarms of Mobile Robots: Towards Versatility with Safety

Authors: Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.
Cite as

Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Swarms of Mobile Robots: Towards Versatility with Safety. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 02:1-02:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{courtieu_et_al:LITES.8.2.2,
  author =	{Courtieu, Pierre and Rieg, Lionel and Tixeuil, S\'{e}bastien and Urbain, Xavier},
  title =	{{Swarms of Mobile Robots: Towards Versatility with Safety}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:36},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.2},
  URN =		{urn:nbn:de:0030-drops-192942},
  doi =		{10.4230/LITES.8.2.2},
  annote =	{Keywords: distributed algorithm, mobile autonomous robots, formal proof}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.10
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities

Authors: Liron Cohen and Vincent Rahli

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Time-progressing expressions, i.e., expressions that compute to different values over time such as Brouwerian choice sequences or reference cells, are a common feature in many frameworks. For type theories to support such elements, they usually employ sheaf models. In this paper, we provide a general framework in the form of an extensional type theory incorporating various time-progressing elements along with a general possible-worlds forcing interpretation parameterized by modalities. The modalities can, in turn, be instantiated with topological spaces of bars, leading to a general sheaf model. This parameterized construction allows us to capture a distinction between theories that are "agnostic", i.e., compatible with classical reasoning in the sense that classical axioms can be validated, and those that are "intuitionistic", i.e., incompatible with classical reasoning in the sense that classical axioms can be proven false. This distinction is made via properties of the modalities selected to model the theory and consequently via the space of bars instantiating the modalities. We further identify a class of time-progressing elements that allows deriving "intuitionistic" theories that include not only choice sequences but also simpler operators, namely reference cells.
Cite as

Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.FSCD.2022.10,
  author =	{Cohen, Liron and Rahli, Vincent},
  title =	{{Constructing Unprejudiced Extensional Type Theories with Choices via Modalities}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.10},
  URN =		{urn:nbn:de:0030-drops-162917},
  doi =		{10.4230/LIPIcs.FSCD.2022.10},
  annote =	{Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.11
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle

Authors: Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.
Cite as

Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bickford_et_al:LIPIcs.CSL.2021.11,
  author =	{Bickford, Mark and Cohen, Liron and Constable, Robert L. and Rahli, Vincent},
  title =	{{Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.11},
  URN =		{urn:nbn:de:0030-drops-134455},
  doi =		{10.4230/LIPIcs.CSL.2021.11},
  annote =	{Keywords: Intuitionism, Extensional type theory, Constructive Type Theory, Realizability, Choice sequences, Classical Logic, Law of Excluded Middle, Theorem proving, Coq}
}
  • Refine by Type
  • 14 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 7 2025
  • 2 2023
  • 2 2022
  • 1 2021

  • Refine by Author
  • 6 Rahli, Vincent
  • 5 Cohen, Liron
  • 2 Locher, Thomas
  • 2 Tosun, Ayberk
  • 2 da Rocha Paiva, Bruno
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 6 Theory of computation → Constructive mathematics
  • 5 Theory of computation → Distributed algorithms
  • 5 Theory of computation → Type theory
  • 3 Computer systems organization → Fault-tolerant network topologies
  • 1 Computer systems organization → Availability
  • Show More...

  • Refine by Keyword
  • 4 Constructive Type Theory
  • 4 Realizability
  • 4 Theorem proving
  • 3 Agda
  • 3 Continuity
  • 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