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

DOI10.1016/J.COMGEO.2010.06.006MaRDI QIDQ448980zbMATH OpenOpenAlexFDO

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

Publication date 11 September 2012

Published in Computational Geometry (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.comgeo.2010.06.006

zbMATH Keywords

computational geometryconvex hullformal specificationsCoq systemcomputer-aided proofshypermaps

Mathematics Subject Classification ID

Packaged methods for numerical algorithms (65Y15) Numerical aspects of computer graphics, image analysis, and computational geometry (65D18)

Recommendations

• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• scientific article; zbMATH DE number 1863395
• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Discrete Jordan curve theorem: a proof formalized in Coq with hypermaps

Cites work

• scientific article; zbMATH DE number 3841211 (Why is no real title available?)
• scientific article; zbMATH DE number 4032498 (Why is no real title available?)
• scientific article; zbMATH DE number 3489159 (Why is no real title available?)
• scientific article; zbMATH DE number 1220053 (Why is no real title available?)
• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• scientific article; zbMATH DE number 3338383 (Why is no real title available?)
• A proof of GMP square root
• An introduction to small scale reflection in Coq
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Automated Deduction in Geometry
• Axioms and hulls
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Classroom examples of robustness problems in geometric computations
• Combinatorial Oriented Maps
• Computational geometry. Algorithms and applications.
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Discrete Jordan curve theorem: a proof formalized in Coq with hypermaps
• Formal proof - the four color theorem
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to algorithms
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps

Cited in

(13)

• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• Formal specification and proofs for the topology and classification of combinatorial surfaces
• Tests and proofs for custom data generators
• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Theorem Proving in Higher Order Logics
• Formal study of plane Delaunay triangulation
• A verified ODE solver and the Lorenz attractor
• Verification of Closest Pair of Points Algorithms
• Formal study of functional orbits in finite domains
• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Tests and Proofs for Enumerative Combinatorics
• Hypermap specification and certified linked implementation using orbits

Describes a project that uses

Uses Software

• OCaml
• Coq

This page was built for publication: Designing and proving correct a convex hull algorithm with hypermaps in Coq

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