### Abstract

This entry provides two related verified divide-and-conquer algorithms
solving the fundamental

BSD License*Closest Pair of Points*problem in Computational Geometry. Functional correctness and the optimal running time of*O*(*n*log*n*) are proved. Executable code is generated which is empirically competitive with handwritten reference implementations.### Change history

[2020-14-04] Incorporate Time_Monad of the AFP entry Root_Balanced_Tree.