Formal proof in Coq and derivation of an imperative program to compute convex hulls

DOI10.1007/978-3-642-40672-0_6MaRDI QIDQ2849508zbMATH OpenOpenAlexFDO

Authors Christophe Brun, Jean-François Dufourd, Nicolas Magaud

Publication date 20 September 2013

Published in Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00916880/file/CH-submitted2011.pdf

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Computational aspects related to convexity (52B55)

Recommendations

• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• scientific article; zbMATH DE number 1863395
• Automated Deduction in Geometry

Cited in

(8)

• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Formalization of the Poincaré disc model of hyperbolic geometry
• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Theorem Proving in Higher Order Logics
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Design and formal proof of a new optimal image segmentation program with hypermaps

Describes a project that uses

Uses Software

• OCaml
• Coq

This page was built for publication: Formal proof in Coq and derivation of an imperative program to compute convex hulls

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2849508)