### Abstract

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.