Closest_Pair_Points
| swMATH ID: | 47255 |
| Software Authors: | Rau, Martin; Nipkow, Tobias |
| Description: | Closest Pair of Points Algorithms. 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. |
| Homepage: | https://www.isa-afp.org/entries/Closest_Pair_Points.html |
| Dependencies: | Isabelle/HOL |
| Related Software: | Root Balanced Tree; Archive Formal Proofs; Isabelle/HOL |
| Cited in: | 1 Document |
Cited by 2 Authors
| 1 | Nipkow, Tobias |
| 1 | Rau, Martin |
Cited in 0 Serials
Cited in 1 Field
| 1 | Computer science (68-XX) |
