Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. - Christophe Brun; Jean-François Dufourd; Nicolas Magaud (Automated Deduction in Geometry, 2012)

Designing and proving correct a convex hull algorithm with hypermaps in Coq. - Christophe Brun; Jean-François Dufourd; Nicolas Magaud (Comput. Geom., 2012)