Skip to Main content Skip to Navigation
Conference papers

Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls

Abstract : This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00916880
Contributor : Nicolas Magaud <>
Submitted on : Tuesday, December 10, 2013 - 8:13:20 PM
Last modification on : Saturday, January 13, 2018 - 1:02:58 AM
Long-term archiving on: : Tuesday, March 11, 2014 - 4:30:11 PM

File

CH-submitted2011.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Christophe Brun, Jean-François Dufourd, Nicolas Magaud. Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls. Automated Deduction in Geometry (Post-proceedings), Sep 2012, Edinbourg, United Kingdom. pp.71-88, ⟨10.1007/978-3-642-40672-0_6⟩. ⟨hal-00916880⟩

Share

Metrics

Record views

208

Files downloads

840