Designing and proving correct a convex hull algorithm with hypermaps in Coq
From MaRDI portal
Publication:448980
DOI10.1016/j.comgeo.2010.06.006zbMath1247.65021OpenAlexW2166210250MaRDI QIDQ448980
Christophe Brun, Nicolas Magaud, Jean-François Dufourd
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
Numerical aspects of computer graphics, image analysis, and computational geometry (65D18) Packaged methods for numerical algorithms (65Y15)
Related Items (6)
Tests and proofs for custom data generators ⋮ Verification of Closest Pair of Points Algorithms ⋮ A verified ODE solver and the Lorenz attractor ⋮ Formal specification and proofs for the topology and classification of combinatorial surfaces ⋮ Formal study of functional orbits in finite domains ⋮ Tests and Proofs for Enumerative Combinatorics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- 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
- Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
- Axioms and hulls
- A proof of GMP square root
- Classroom examples of robustness problems in geometric computations
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Combinatorial Oriented Maps
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Automated Deduction in Geometry
This page was built for publication: Designing and proving correct a convex hull algorithm with hypermaps in Coq
