Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art : The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, N. Magaud, and P. Zimmermann, A Proof of GMP Square Root, Journal of Automated Reasoning, vol.29, issue.3/4, pp.225-252, 2002.
DOI : 10.1023/A:1021987403425
URL : https://hal.archives-ouvertes.fr/inria-00101044

Y. Bertrand, J. Dufourd, J. Françon, and P. Lienhardt, Algebraic specification and development in geometric modeling, TAPSOFT'93: Theory and Practice of Software Development, pp.75-89, 1993.
DOI : 10.1007/3-540-56610-4_57

C. Brun, J. Dufourd, and N. Magaud, Formal Proof of the Incremental Convex Hull Algorithm

C. Brun, J. Dufourd, and N. Magaud, Designing and proving correct a convex hull algorithm with hypermaps in Coq, Computational Geometry, vol.45, issue.8, p.2010
DOI : 10.1016/j.comgeo.2010.06.006
URL : https://hal.archives-ouvertes.fr/hal-00955400

C. Development and T. , The Coq Proof Assistant -Reference Manual and Library

R. Cori, Un code pour les graphes planaires et ses applications, Astérisque, vol.27, 1970.

J. Dufourd, Design and formal proof of a new optimal image segmentation program with hypermaps, Pattern Recognition, vol.40, issue.11, pp.2974-2993, 2007.
DOI : 10.1016/j.patcog.2007.02.013

J. Dufourd, An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps, Journal of Automated Reasoning, vol.47, issue.5, pp.19-51, 2009.
DOI : 10.1007/s10817-009-9117-x

J. Dufourd and Y. Bertot, Formal Study of Plane Delaunay Triangulation, Interactive Theorem Proving, pp.211-226, 2010.
DOI : 10.1007/978-3-642-14052-5_16
URL : https://hal.archives-ouvertes.fr/inria-00504027

H. Edelsbrunner, Algorithms in Combinatorial Geometry. Monographs in Theoretical Computer Science. An EATCS Series, 1987.

E. Flato, D. Halperin, I. Hanniel, O. Nechushtan, and E. Ezra, The Design and Implementation of Planar Maps in CGAL, WAE'99: Algorithm Engineering, pp.154-168, 1999.
DOI : 10.1007/3-540-48318-7_14

G. Gonthier, Formal Proof -The Four-Colour Theorem, Notices of the AMS, vol.55, issue.11, pp.1382-1393, 2008.

I. Team and . Cgogn, Combinatorial and Geometric mOdeling with Generic Ndimensional Maps

P. Lienhardt, Topological models for boundary representation: a comparison with n-dimensional generalized maps, Computer-Aided Design, vol.23, issue.11, pp.59-82, 1991.
DOI : 10.1016/0010-4485(91)90100-B

L. Meikle and J. Fleuriot, Mechanical Theorem Proving in Computational Geometry, Automated Deduction in Geometry, pp.1-18, 2006.
DOI : 10.1007/11615798_1

D. Pichardie and Y. Bertot, Formalizing Convex Hull Algorithms, Theorem Proving in Higher Order Logics, pp.346-361, 2001.
DOI : 10.1007/3-540-44755-5_24