Distributed algorithms are expressed as axiomatic theories in three-valued modal logic over semitopologies, with examples including Bracha broadcast and Crusader agreement, and all proofs formalized in Lean 4.
Available at https://arxiv.org/abs/2502.00892
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
cs.LO 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies
Distributed algorithms are expressed as axiomatic theories in three-valued modal logic over semitopologies, with examples including Bracha broadcast and Crusader agreement, and all proofs formalized in Lean 4.