#### Verification of Closest Pair of Points Algorithms

We verify two related divide-and-conquer algorithms solving one of the
fundamental problems in Computational Geometry, the Closest Pair of
Points problem. Using the interactive theorem prover Isabelle/HOL, we
prove functional correctness and the optimal running time of *O(n log n)*
of the algorithms. We generate executable code which is empirically
competitive with handwritten reference implementations.
pdf
Spinger web page

BibTeX:

@inproceedings{RauN-IJCAR20,
author={Martin Rau and Tobias Nipkow},
title={Verification of Closest Pair of Points Algorithms},
booktitle={Automated Reasoning (IJCAR 2020)},
editor={N. Peltier and V. Sofronie-Stokkermans},publisher={Springer},
series={LNCS},volume={12167},pages={291--306},year=2020}

Isabelle theories in the
Archive of Formal Proofs