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.
Type de document :
Article dans une revue
Computational Geometry, Elsevier, 2012, 45 (8), pp.436-457. 〈10.1016/j.comgeo.2010.06.006〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00955400
Contributeur : Nicolas Magaud <>
Soumis le : mardi 4 mars 2014 - 14:25:48
Dernière modification le : jeudi 11 janvier 2018 - 06:22:39
Document(s) archivé(s) le : mercredi 4 juin 2014 - 11:36:18

Fichier

CGTA2012-BrunDufourdMagaud.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

160