Twenty years ago, Herlihy/Shavit and Saks/Zaharoglou won the Gödel prize for the introduction of a simplicial semantics for distributed computing. This line of work culminated in a characterization of the distributed tasks which can be solved by asynchronous wait-free systems, resulting in the Asynchronous Computability Theorem (ACT). In this paper, we extend this semantics by identifying spectral topology as the natural generalization of the finite combinatorial topology they employed. In particular, we extend the topological approach of ACT to any round-based, content-neutral, full-information protocol. This family of protocols contains the Iterated Immediate Snapshot model (IIS), to which many distributed computation models can be reduced. In this sense, our work provides first steps towards a unified topological framework for distributed computing. The main insight of this work is in considering global states obtained after finite executions of a distributed protocol not as abstract simplicial complexes as was previously done, but as finite spectral spaces, considering the Alexandrov topology on the associated face posets. Using this point-set topological approach, coupled with the interpretation of a distributed protocol as an endofunctor Π on the category of simplicial complexes, we show that any initial configuration ℐ can be associated to a projective limit system of finite complexes. The limit thereof is a spectral space Π^∞(ℐ) which precisely encodes the behavior of the protocol presented by Π. This leads us to derive a new general distributed computability theorem using Stone duality: a protocol Π solves a colorless task (ℐ,𝒪,Δ) if and only if there exists a spectral map f:Π^∞(ℐ) → 𝒪 compatible with Δ. From this general characterization, we derive known colorless computability theorems, and provide new insights into the previously established connection between task-solvability and continuous maps between geometric realizations. This is achieved through Stone duality, a well established tool for such tight correspondences in computer science.

We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.