Email Gateway (Dec 27 2025 at 17:22): Email Gateway (Dec 27 2025 at 17:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry, Set Reconciliation, by Paul Hofmeier and Emin Karayel.
This entry formally verifies the set reconciliation algorithm with nearly optimal communication complexity, due to Y. Minsky et al. [1]. The algorithm allows two communication partners, who have a similar pair of sets, to reconcile them while using messages of nearly optimal size, proportional to a bound on the maximum symmetric difference between the sets. The formalization also introduces an optimization, which reduces the communication complexity even further compared to the original publication.
https://www.isa-afp.org/entries/Set_Reconciliation.html
Last updated: Jan 11 2026 at 16:28 UTC