| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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. |
| Change history: | [2020-14-04]: Incorporate Time_Monad of the AFP entry Root_Balanced_Tree. |
| 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, Root_Balanced_Tree |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |