Rabin's Closest Pair of Points Algorithm

This entry formalizes Rabin’s randomized algorithm for the closest pair of points problem with expected linear running time. Remarkable is that the best-known deterministic algorithms have super-linear running times. Hence this algorithm is one of the first known examples of randomized algorithms that outperform deterministic algorithms. The formalization also introduces a probabilistic time monad, which builds on the existing deterministic time monad.