pith. sign in

arxiv: 2512.21137 · v3 · pith:EP4UJQ5Cnew · submitted 2025-12-24 · 💻 cs.LO · cs.DC

Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies

Murdoch J. Gabbay This is my paper

Pith reviewed 2026-05-16 19:48 UTC · model grok-4.3

classification 💻 cs.LO cs.DC
keywords distributed algorithmsmodal logicsemitopologiesaxiomatic theoriesBracha broadcastCrusader agreementdeclarative specificationLean 4
0
0 comments X

The pith

Distributed algorithms admit declarative axiomatizations in three-valued modal logic over semitopologies.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to express the essential properties of distributed algorithms as axiomatic theories inside three-valued modal logic defined over semitopologies. It works through three examples: a simple voting protocol, Bracha Broadcast, and Crusader Agreement, each presented as a compact set of logical axioms rather than a description of state transitions. The resulting specifications remain human-readable while supporting precise reasoning about correctness and resilience. All proofs are formalized in Lean 4, and the same method has already revealed errors in a proposed industrial protocol. A reader would see this as shifting protocol specification from imperative state machines to declarative logical theories.

Core claim

Distributed algorithms can be specified as declarative axiomatic theories in three-valued modal logic over semitopologies. This is shown by constructing axiomatizations of Declarative Bracha Broadcast and Declarative Crusader Agreement that isolate the logical essence of each protocol while abstracting away explicit state transitions of any implementing machine.

What carries the argument

Three-valued modal logic over semitopologies, which encodes declarative correctness and resilience properties by treating system states as open sets and truth values as three-way to accommodate partial information and failures.

If this is right

  • Axiomatic theories supply specifications that are more precise than natural-language descriptions yet more abstract than source code or transition-system models.
  • Reasoning about correctness, resilience, and failure becomes possible inside a single logical framework.
  • The same specifications can serve as a foundation for both human review and machine-assisted verification efforts.
  • Design improvements and alternative implementations can be explored by manipulating the axioms rather than rewriting code.
  • The approach scales to industrial protocols and has already been used to detect specification errors.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could be applied to other families of distributed algorithms such as consensus or leader-election protocols.
  • Lean 4 formalization makes it feasible to connect these axiomatizations with existing libraries for distributed-systems verification.
  • Logical-level comparison between protocol variants becomes straightforward once both are expressed in the same axiomatic language.
  • Wider adoption might encourage protocol designers to publish axiomatic specifications alongside pseudocode.

Load-bearing premise

That three-valued modal logic over semitopologies can capture every essential correctness and resilience property of the target algorithms without omitting behavioral details that only appear in concrete executions.

What would settle it

A concrete execution trace of Bracha Broadcast or Crusader Agreement in which all the logical axioms hold yet the protocol violates its intended safety or liveness guarantee, or a correct execution in which the axioms fail to hold.

Figures

Figures reproduced from arXiv: 2512.21137 by Murdoch J. Gabbay.

Figure 1
Figure 1. Figure 1: Truth-tables for some operations on 3 = {t, b,f} (Definition 2.2.1) Define a unary connective ¬ (negation), and binary connectives ∧ (conjunction), ∨ (disjunction), → (weak implication), ⇀ (strong implication), ≡ (identity), and ⊕ (exclusive-or), and define modalities T, B, F, TB, and TF, as in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A simple voting protocol (Definition 2.5.1) Proof. By inspection of the truth-tables in [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Syntax of a simple modal logic (Definition [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Denotation for a simple modal logic (Definition [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Informal (English) description of Bracha Broadcast (Remark [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: ThyBB: axioms of Bracha Broadcast (Definition 4.1.2) (BrValidity?) ThyBB ⊨µ ✸bcst(v) → ✷dlvr(v) (Proposition 4.2.9) (BrNoDup) ThyBB ⊨µ ∃01 dlvr (Proposition 4.2.11) (BrIntegrity) ThyBB ⊨µ dlvr(v) → ✸bcst(v) (Proposition 4.2.12) (BrConsistency) ThyBB ⊨µ ∃01✸dlvr(v) (Proposition 4.2.11) (BrTotality) ThyBB ⊨µ ✸dlvr(v) → ✷dlvr(v) (Proposition 4.2.13) [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Correctness properties for ThyBB (Remark 4.2.2) So in this paper, we assume a model is just presented to us, and our business is to check whether it validates axioms. All of the complexity inherent in studying an implementation – i.e. a machine to compute such a model – is elided by design. Remark 4.1.4 As for our voting example from [PITH_FULL_IMAGE:figures/full_fig_p013_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Pseudocode Crusader Agreement algorithm from [ [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: ThyCA: axioms of Crusader Agreement (Definition 5.1.2) (CaAgree) ThyCA ⊨µ (✸output(v) ∧ ✸output(v ′ )) ⇀ v=v ′ (Proposition 5.3.2) (CaValid1) ThyCA ⊨µ (TB✷input(v) ∧ output(v ′ )) ⇀ v=v ′ (Proposition 5.3.5) (CaValid2) ThyCA ⊨µ ✸output(v) ⇀ ✸input(v) (Proposition 5.3.5) (CaLive) ThyCA ⊨µ ✷ ∃v.output(v) (Proposition 5.3.10) [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Correctness properties for ThyCA (Definition 5.1.4) These become ThyCA ⊨µ (✷input(v) ∧ output(v ′ ))⇀ v=v ′ and ThyCA ⊨µ ✸output(v)⇀✸input(v). See Proposition 5.3.5. (3) Liveness: If all non-faulty parties start the protocol then all non-faulty parties eventually output a value. This becomes ThyCA ⊨µ ✷ ∃v.output(v). See Proposition 5.3.10. 5.2 Discussion of the axioms Remark 5.2.1 As for the axioms in Fig… view at source ↗
read the original abstract

We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript proposes specifying distributed algorithms declaratively as axiomatic theories in three-valued modal logic over semitopologies. It illustrates the method with a voting protocol, Bracha Broadcast, and Crusader Agreement, provides Lean 4 formalizations of the axioms and derived properties, and claims the approach yields compact, human-readable specifications that capture essential correctness and resilience properties while abstracting from operational state transitions.

Significance. If the axiomatizations prove adequate, the framework offers a high-level alternative to imperative or state-machine specifications for distributed protocols, enabling more abstract reasoning about resilience and failure modes. The Lean 4 formalization is a clear strength, supplying machine-checked evidence of internal consistency for the presented axioms and derivations.

major comments (1)
  1. [Sections introducing Declarative Bracha Broadcast and Declarative Crusader Agreement (and the discussion of their formal] The manuscript provides no explicit soundness or adequacy theorem establishing that satisfaction of the modal axioms (e.g., those for Declarative Bracha Broadcast) in the semitopological semantics entails or is entailed by correctness in the standard asynchronous Byzantine message-passing model. This link is load-bearing for the claim that the declarative theories faithfully capture resilience properties such as validity and consistency under <n/3 faults; without it, omitted execution details (scheduling, fault timing, message patterns) could render the axioms either too strong or too weak relative to the concrete protocols.
minor comments (1)
  1. [Abstract] Abstract contains the typo 'Bracha Broacast' (should be 'Bracha Broadcast').

Simulated Author's Rebuttal

1 responses · 1 unresolved

We thank the referee for their careful reading of the manuscript and for identifying the need to clarify the relationship between our declarative axiomatizations and the standard operational model. We respond to the major comment below.

read point-by-point responses

  1. Referee: [Sections introducing Declarative Bracha Broadcast and Declarative Crusader Agreement (and the discussion of their formal] The manuscript provides no explicit soundness or adequacy theorem establishing that satisfaction of the modal axioms (e.g., those for Declarative Bracha Broadcast) in the semitopological semantics entails or is entailed by correctness in the standard asynchronous Byzantine message-passing model. This link is load-bearing for the claim that the declarative theories faithfully capture resilience properties such as validity and consistency under <n/3 faults; without it, omitted execution details (scheduling, fault timing, message patterns) could render the axioms either too strong or too weak relative to the concrete protocols.

    Authors: The semitopological semantics is constructed precisely to encode the quorum intersection properties that guarantee resilience under <n/3 Byzantine faults in the standard model; the axioms for Declarative Bracha Broadcast and Crusader Agreement are the minimal set of modal statements that express validity and consistency directly in this semantics. The Lean 4 formalization verifies that these axioms are consistent and that the expected resilience properties are derivable within the logic. We do not claim a full bisimulation or adequacy theorem relating every possible execution trace in the asynchronous message-passing model to satisfaction of the axioms, as the declarative approach deliberately abstracts away scheduling and message-order details. Any concrete protocol whose communication graph satisfies the semitopological assumptions will satisfy the axioms; the axioms are therefore neither arbitrarily strong nor weak relative to the resilience conditions they are intended to capture. A detailed soundness proof would constitute a separate technical contribution and lies outside the scope of the present paper. revision: no

standing simulated objections not resolved
  • Absence of an explicit soundness or adequacy theorem linking satisfaction of the modal axioms in the semitopological semantics to correctness in the standard asynchronous Byzantine message-passing model.

Circularity Check

0 steps flagged

No significant circularity; derivations are self-contained via external Lean formalization

full rationale

The paper defines axiomatic theories for protocols such as Declarative Bracha Broadcast and Declarative Crusader Agreement directly in three-valued modal logic over semitopologies, then formalizes the proofs of derived properties in Lean 4. No step reduces a claimed prediction or correctness result to a parameter fitted from that same result, nor does any load-bearing premise collapse to a self-citation chain or definitional renaming. The Lean formalization supplies independent machine-checked verification of the internal derivations, and the declarative specifications are presented as illustrative axiomatizations rather than outputs forced by construction from operational semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the assumption that the chosen modal logic and semitopology structure are adequate to express protocol properties; no numerical free parameters are mentioned, and no new physical entities are postulated.

axioms (2)
  • standard math Axioms of three-valued modal logic
    The paper adopts an existing three-valued modal logic as the specification language.
  • domain assumption Semitopology axioms for network connectivity
    Semitopologies are used to model the topological properties of distributed systems under failure.

pith-pipeline@v0.9.0 · 5537 in / 1332 out tokens · 34256 ms · 2026-05-16T19:48:45.345253+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

  1. [1]

    1-3, 31--60

    Ofer Arieli, Arnon Avron, and Anna Zamansky, Ideal paraconsistent logics, Studia Logica 99 (2011), no. 1-3, 31--60

    work page 2011

  2. [2]

    Ittai Abraham, Naama Ben-David, and Sravya Yandamuri, Efficient and adaptively secure asynchronous binary agreement via binding crusader agreement, Proceedings of the 2022 ACM Symposium on Principles of Distributed Computing (New York, NY, USA), PODC'22, Association for Computing Machinery, 2022, Available online at https://eprint.iacr.org/2022/711.pdf, p...

    work page 2022

  3. [3]

    184, Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2020, pp

    Ignacio Amores - Sesar, Christian Cachin, and Jovana Micic, Security analysis of R ipple consensus , 24th International Conference on Principles of Distributed Systems, OPODIS 2020, December 14-16, 2020, Strasbourg, France (Virtual Conference) (Quentin Bramas, Rotem Oshman, and Paolo Romano, eds.), LIPIcs, vol. 184, Schloss Dagstuhl - Leibniz-Zentrum f \"...

    work page 2020

  4. [4]

    253, Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2022, pp

    Ignacio Amores - Sesar, Christian Cachin, and Enrico Tedeschi, When is spring coming? A security analysis of A valanche consensus , 26th International Conference on Principles of Distributed Systems, OPODIS 2022, December 13-15, 2022, Brussels, Belgium (Eshcar Hillel, Roberto Palmieri, and Etienne Rivi \` e re, eds.), LIPIcs, vol. 253, Schloss Dagstuhl - ...

    work page 2022

  5. [5]

    3, 247--277

    Orestis Alpos, Christian Cachin, Bj \" o rn Tackmann, and Luca Zanolini, Asymmetric distributed trust, Distributed Computing 37 (2024), no. 3, 247--277

    work page 2024

  6. [6]

    Ethan Buchman, Jae Kwon, and Zarko Milosevic, The latest gossip on BFT consensus , CoRR abs/1807.04938 (2018)

    work page arXiv 2018

  7. [7]

    2, 130--143

    Gabriel Bracha, Asynchronous byzantine agreement protocols, Information and Computation 75 (1987), no. 2, 130--143

    work page 1987

  8. [8]

    Christian Cachin, Rachid Guerraoui, and Lu \' s E. T. Rodrigues, Introduction to reliable and secure distributed programming (2. ed.) , Springer, 2011

    work page 2011

  9. [9]

    Seltzer and Paul J

    Miguel Castro and Barbara Liskov, Practical byzantine fault tolerance, Proceedings of the Third USENIX Symposium on Operating Systems Design and Implementation (OSDI), New Orleans, Louisiana, USA, February 22-25, 1999 (Margo I. Seltzer and Paul J. Leach, eds.), USENIX Association, 1999, pp. 173--186

    work page 1999

  10. [10]

    George Danezis, Lefteris Kokoris - Kogias, Alberto Sonnino, and Alexander Spiegelman, Narwhal and tusk: a dag-based mempool and efficient BFT consensus , EuroSys '22: Seventeenth European Conference on Computer Systems, Rennes, France, April 5 - 8, 2022 (Y \' e rom - David Bromberg, Anne - Marie Kermarrec, and Christos Kozyrakis, eds.), ACM , 2022, pp. 34--50

    work page 2022

  11. [11]

    Gabbay, Semitopology: decentralised collaborative action via topology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651

    Murdoch J. Gabbay, Semitopology: decentralised collaborative action via topology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651

    work page 2024

  12. [12]

    , Semitopology: a topological approach to decentralised collaborative action, The Journal of Logic and Computation (2025), https://doi.org/10.1093/logcom/exae050

    work page doi:10.1093/logcom/exae050 2025

  13. [13]

    Murdoch J. Gabbay, Arvid Jakobsson, and Kristina Sojakova, Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard , 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021) (Dagstuhl, Germany) (Bruno Bernardo and Diego Marmsoler, eds.), Open Access Series in Informatics (OASIcs), vol. 95, Schloss Dagstuhl -- Leibniz-Zentrum f \"u r...

    work page 2021

  14. [14]

    Gabbay and Luca Zanolini, A declarative approach to specifying distributed algorithms using three-valued modal logic, 2 2025

    Murdoch J. Gabbay and Luca Zanolini, A declarative approach to specifying distributed algorithms using three-valued modal logic, 2 2025

    work page 2025

  15. [15]

    Available at https://arxiv.org/abs/2502.00892

    , A declarative approach to specifying distributed algorithms using three-valued modal logic, 2025, Journal draft submitted for publication. Available at https://arxiv.org/abs/2502.00892

    work page arXiv 2025

  16. [16]

    Maurice Herlihy, Dmitry Kozlov, and Sergio Rajsbaum, Distributed computing through combinatorial topology, Morgan Kaufmann, 2013

    work page 2013

  17. [17]

    Sravya Yandamuri Ittai Abraham, Naama Ben-David, Asynchronous agreement part 4: Crusader agreement and binding crusader agreement, https://decentralizedthoughts.github.io/2022-04-05-aa-part-four-CA-and-BCA/ https://decentralizedthoughts.github.io/2022-04-05-aa-part-four-CA-and-BCA/ (permalink https://web.archive.org/web/20250624133701/https://decentralize...

    work page arXiv 2022

  18. [18]

    Korhonen, eds.), ACM , 2021, pp

    Idit Keidar, Eleftherios Kokoris - Kogias, Oded Naor, and Alexander Spiegelman, All you need is DAG , PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021 (Avery Miller, Keren Censor - Hillel, and Janne H. Korhonen, eds.), ACM , 2021, pp. 165--175

    work page 2021

  19. [19]

    310, 2019, pp

    Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts, The TLA+ toolbox , Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019 (Rosemary Monahan, Virgile Prevosto, and Jos \' e Proen c a, eds.), EPTCS , vol. 310, 2019, pp. 50--62

    work page 2019

  20. [20]

    Leslie Lamport, The temporal logic of actions, ACM Trans. Program. Lang. Syst. 16 (1994), no. 3, 872--923

    work page 1994

  21. [21]

    , Specifying systems, the TLA+ language and tools for hardware and software engineers , Addison-Wesley, 2002

    work page 2002

  22. [22]

    Reiter, Byzantine quorum systems, Distributed Computing 11 (1998), no

    Dahlia Malkhi and Michael K. Reiter, Byzantine quorum systems, Distributed Computing 11 (1998), no. 4, 203--213

    work page 1998

  23. [23]

    446--465

    Joachim Neu, Ertem Nusret Tas, and David Tse, Ebb-and-flow protocols: A resolution of the availability-finality dilemma , 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, IEEE , 2021, pp. 446--465

    work page 2021

  24. [24]

    Gabbay and F

    Graham Priest, Paraconsistent logic, Handbook of Philosophical Logic, 2nd Edition (D.M. Gabbay and F. Guenthner, eds.), vol. 6, Kluwer, 2002, pp. 287--393

    work page 2002

  25. [25]

    10625, Springer, 2017, pp

    Rafael Pass and Elaine Shi, The sleepy model of consensus, Advances in Cryptology - ASIACRYPT 2017 - 23rd International Conference on the Theory and Applications of Cryptology and Information Security, Hong Kong, China, December 3-7, 2017, Proceedings, Part II (Tsuyoshi Takagi and Thomas Peyrin, eds.), Lecture Notes in Computer Science, vol. 10625, Spring...

    work page 2017

  26. [26]

    2705--2718

    Alexander Spiegelman, Neil Giridharan, Alberto Sonnino, and Lefteris Kokoris - Kogias, Bullshark: DAG BFT protocols made practical , Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022 (Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi, eds.), ACM , 2022, pp. 2705--2718

    work page 2022

  27. [27]

    Victor Shoup, Proof of history: What is it good for?, May 2022, https://www.shoup.net/papers/poh.pdf

    work page 2022

  28. [28]

    Garay, eds.), Lecture Notes in Computer Science, vol

    Caspar Schwarz - Schilling, Joachim Neu, Barnab \' e Monnot, Aditya Asgaonkar, Ertem Nusret Tas, and David Tse, Three attacks on proof-of-stake ethereum, Financial Cryptography and Data Security - 26th International Conference, FC 2022, Grenada, May 2-6, 2022, Revised Selected Papers (Ittay Eyal and Juan A. Garay, eds.), Lecture Notes in Computer Science,...

    work page 2022

  29. [29]

    Monien and R

    Nicola Santoro and Peter Widmayer, Time is not a healer, STACS 89 (Berlin, Heidelberg) (B. Monien and R. Cori, eds.), Springer Berlin Heidelberg, 1989, pp. 304--313

    work page 1989

  30. [30]

    Myers, Heterogeneous paxos: Technical report, 2020, https://arxiv.org/abs/2011.08253

    Isaac Sheff, Xinwen Wang, Robbert van Renesse, and Andrew C. Myers, Heterogeneous paxos: Technical report, 2020, https://arxiv.org/abs/2011.08253

    work page arXiv 2020

  31. [31]

    Isaac Sheff, Xinwen Wang, Robbert van Renesse, and Andrew C. Myers, Heterogeneous Paxos , 24th International Conference on Principles of Distributed Systems (OPODIS 2020) (Dagstuhl, Germany) (Quentin Bramas, Rotem Oshman, and Paolo Romano, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 184, Schloss Dagstuhl -- Leibniz-Zentrum f \"u...

    work page 2020

  32. [32]

    Yakovenko, Solana: A new architecture for a high performance blockchain v0.8.13, Whitepaper, 2018, https://solana.com/solana-whitepaper.pdf

    A. Yakovenko, Solana: A new architecture for a high performance blockchain v0.8.13, Whitepaper, 2018, https://solana.com/solana-whitepaper.pdf

    work page 2018

  33. [33]

    1703, Springer, 1999, pp

    Yuan Yu, Panagiotis Manolios, and Leslie Lamport, Model checking TLA\( ^ + \) specifications , Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings (Laurence Pierre and Thomas Kropf, eds.), Lecture Notes in Computer Science, vol. 170...

    work page 1999

  34. [34]

    Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan - Gueta, and Ittai Abraham, Hotstuff: BFT consensus with linearity and responsiveness , Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC 2019, Toronto, ON, Canada, July 29 - August 2, 2019 (Peter Robinson and Faith Ellen, eds.), ACM , 2019, pp. 347--356

    work page 2019

  35. [35]

    , " * write output.state after.block = add.period write newline

    ENTRY address archive author booktitle chapter doi edition editor eid eprint howpublished institution isbn issn journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #...

    work page

  36. [36]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in ":" * " " * FUNCTION f...

    work page