Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls

DOI10.1007/978-3-642-40672-0_6zbMath1396.68111OpenAlexW1468516137MaRDI QIDQ2849508

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

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

Related Items (1)

Formalization of the Poincaré disc model of hyperbolic geometry

Uses Software

• Coq
• OCaml

This page was built for publication: Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls