Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

Designing and proving correct a convex hull algorithm with hypermaps in Coq

Abstract : 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.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Nicolas Magaud Connect in order to contact the contributor
Submitted on : Tuesday, March 4, 2014 - 2:25:48 PM
Last modification on : Thursday, January 11, 2018 - 6:22:39 AM
Long-term archiving on: : Wednesday, June 4, 2014 - 11:36:18 AM


Files produced by the author(s)




Christophe Brun, Jean-François Dufourd, Nicolas Magaud. Designing and proving correct a convex hull algorithm with hypermaps in Coq. Computational Geometry, Elsevier, 2012, 45 (8), pp.436-457. ⟨10.1016/j.comgeo.2010.06.006⟩. ⟨hal-00955400⟩



Record views


Files downloads