### Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq

This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml-program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.

C. Brun , J-F. Dufourd ,

Computational Geometry : Theory and Applications , Volume 45 , Number 8 , page 436--457 - 2012

International journal Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq, Computational Geometry : Theory and Applications, Elsevier ( IF : 0.537, SNIP : 1.053, SJR : 0.355 ), pages 436--457, Volume 45, n° 8, 2012, doi:10.1016/j.comgeo.2010.06.006 Research team : IGG

@Article{2-BDM12,
author = {Brun, C. and Dufourd, J-F. and Magaud, N.},
title = {Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq},
journal = {Computational Geometry : Theory and Applications},
number = {8},
volume = {45},
pages = {436--457},
year = {2012},
publisher = {ELSEVIER},
doi = {10.1016/j.comgeo.2010.06.006},
x-international-audience = {Yes},
x-language = {EN},
url = {http://icube-publis.unistra.fr/2-BDM12}
}


See publications of the same authors