Formal proof in Coq and derivation of an imperative program to compute convex hulls
DOI10.1007/978-3-642-40672-0_6zbMATH Open1396.68111OpenAlexW1468516137MaRDI QIDQ2849508FDOQ2849508
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
Recommendations
Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Computational aspects related to convexity (52B55)
Cited In (8)
- 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
- Title not available (Why is that?)
Uses Software
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)
