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 , N. Magaud

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

@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://publis.icube.unistra.fr/2-BDM12}
}