Closest Pair of Points Algorithms

 

Title: Closest Pair of Points Algorithms
Authors: Martin Rau (martin /dot/ rau /at/ tum /dot/ de) and Tobias Nipkow
Submission date: 2020-01-13
Abstract: 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.
BibTeX:
@article{Closest_Pair_Points-AFP,
  author  = {Martin Rau and Tobias Nipkow},
  title   = {Closest Pair of Points Algorithms},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2020,
  note    = {\url{http://isa-afp.org/entries/Closest_Pair_Points.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Akra_Bazzi