Designing and proving correct a convex hull algorithm with hypermaps in Coq
DOI10.1016/J.COMGEO.2010.06.006zbMATH Open1247.65021OpenAlexW2166210250MaRDI QIDQ448980FDOQ448980
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
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
Packaged methods for numerical algorithms (65Y15) Numerical aspects of computer graphics, image analysis, and computational geometry (65D18)
Cites Work
- Introduction to algorithms
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computational geometry. Algorithms and applications.
- Classroom examples of robustness problems in geometric computations
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- An introduction to small scale reflection in Coq
- Formal proof - the four color theorem
- Axioms and hulls
- Title not available (Why is that?)
- Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
- Title not available (Why is that?)
- Automated Deduction in Geometry
- Title not available (Why is that?)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
- Title not available (Why is that?)
- A proof of GMP square root
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Combinatorial Oriented Maps
- Title not available (Why is that?)
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
Cited In (10)
- Formal specification and proofs for the topology and classification of combinatorial surfaces
- Tests and proofs for custom data generators
- 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
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Tests and Proofs for Enumerative Combinatorics
- Title not available (Why is that?)
Uses Software
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)
