Closest Pair of Points Algorithms

Martin Rau and Tobias Nipkow

13 January 2020


This entry provides two related verified divide-and-conquer algorithms solving the fundamental 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.
BSD License

Change history

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

Depends On