{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:51:32Z","timestamp":1760122292212},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642406713"},{"type":"electronic","value":"9783642406720"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40672-0_6","type":"book-chapter","created":{"date-parts":[[2013,9,2]],"date-time":"2013-09-02T07:49:04Z","timestamp":1378108144000},"page":"71-88","source":"Crossref","is-referenced-by-count":2,"title":["Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Brun","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Magaud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-22110-1_7","volume-title":"Computer Aided Verification","author":"E. Alkassar","year":"2011","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: Verification of Certifying Computations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 67\u201382. Springer, Heidelberg (2011)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"3-4","key":"6_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1021987403425","volume":"29","author":"Y. Bertot","year":"2002","unstructured":"Bertot, Y., Magaud, N., Zimmermann, P.: A Proof of GMP Square Root. Journal of Automated Reasoning\u00a029(3-4), 225\u2013252 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-56610-4_57","volume-title":"TAPSOFT 1993: Theory and Practice of Software Development","author":"Y. Bertrand","year":"1993","unstructured":"Bertrand, Y., Dufourd, J.-F., Fran\u00e7on, J., Lienhardt, P.: Algebraic Specification and Development in Geometric Modeling. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol.\u00a0668, pp. 75\u201389. Springer, Heidelberg (1993)"},{"key":"6_CR5","unstructured":"Brun, C., Dufourd, J.-F., Magaud, N.: Formal Proof of the Incremental Convex Hull Algorithm, \n                  \n                    http:\/\/galapagos.gforge.inria.fr"},{"issue":"8","key":"6_CR6","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1016\/j.comgeo.2010.06.006","volume":"45","author":"C. Brun","year":"2012","unstructured":"Brun, C., Dufourd, J.-F., Magaud, N.: Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq. Computational Geometry, Theory and Applications\u00a045(8), 436\u2013457 (2012)","journal-title":"Computational Geometry, Theory and Applications"},{"key":"6_CR7","unstructured":"CEA-INRIA. The Frama-C Software Verification Toolkit, \n                  \n                    http:\/\/frama-c.cea.fr"},{"key":"6_CR8","unstructured":"Coq Development Team. The Coq Proof Assistant - Reference Manual and Library, \n                  \n                    http:\/\/coq.inria.fr\/"},{"key":"6_CR9","unstructured":"Cori, R.: Un code pour les graphes planaires et ses applications. Ast\u00e9risque, vol.\u00a027. Socie\u00e9t\u00e9 math\u00e9matique de France (1970)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"de Berg, M., Cheong, O., van Kreveld, M., Overmars, M.: Computational Geometry, Algorithms and Applications. Springer (2008)","DOI":"10.1007\/978-3-540-77974-2"},{"issue":"11","key":"6_CR11","doi-asserted-by":"publisher","first-page":"2974","DOI":"10.1016\/j.patcog.2007.02.013","volume":"40","author":"J.-F. Dufourd","year":"2007","unstructured":"Dufourd, J.-F.: Design and Formal Proof of a New Optimal Image Segmentation Program with Hypermaps. Pattern Recognition\u00a040(11), 2974\u20132993 (2007)","journal-title":"Pattern Recognition"},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/s10817-009-9117-x","volume":"43","author":"J.-F. Dufourd","year":"2009","unstructured":"Dufourd, J.-F.: An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. Journal of Automated Reasoning\u00a043(1), 19\u201351 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-14052-5_16","volume-title":"Interactive Theorem Proving","author":"J.-F. Dufourd","year":"2010","unstructured":"Dufourd, J.-F., Bertot, Y.: Formal Study of Plane Delaunay Triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 211\u2013226. Springer, Heidelberg (2010)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Edelsbrunner, H.: Algorithms in Combinatorial Geometry. Monographs in Theoretical Computer Science, An EATCS Series. Springer (1987)","DOI":"10.1007\/978-3-642-61568-9"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-48318-7_14","volume-title":"Algorithm Engineering","author":"E. Flato","year":"1999","unstructured":"Flato, E., Halperin, D., Hanniel, I., Nechushtan, O.: The Design and Implementation of Planar Maps in CGAL. In: Vitter, J.S., Zaroliagis, C.D. (eds.) WAE 1999. LNCS, vol.\u00a01668, pp. 154\u2013168. Springer, Heidelberg (1999)"},{"issue":"11","key":"6_CR16","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal Proof - The Four-Colour Theorem. Notices of the AMS\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the AMS"},{"key":"6_CR17","unstructured":"IGG Team. CGoGN: Combinatorial and Geometric mOdeling with Generic N-dimensional Maps, \n                  \n                    https:\/\/iggservis.u-strasbg.fr\/CGoGN\/"},{"issue":"1","key":"6_CR18","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.comgeo.2007.06.003","volume":"40","author":"L. Kettner","year":"2008","unstructured":"Kettner, L., Mehlhorn, K., Pion, S., Schirra, S., Yap, C.-K.: Classroom Examples of Robustness Problems in Geometric Computations. Computational Geometry\u00a040(1), 61\u201378 (2008)","journal-title":"Computational Geometry"},{"key":"6_CR19","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55611-7","volume-title":"Axioms and Hulls","author":"D.E. Knuth","year":"1992","unstructured":"Knuth, D.E.: Axioms and Hulls. LNCS, vol.\u00a0606. Springer, Heidelberg (1992)"},{"key":"6_CR20","first-page":"59","volume":"23","author":"P. Lienhardt","year":"1991","unstructured":"Lienhardt, P.: Topological Models for Boundary Representation: a Comparison with n-Dimensional Generalized Maps. Computer-Aided Design\u00a023, 59\u201382 (1991)","journal-title":"Computer-Aided Design"},{"key":"6_CR21","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11615798_1","volume-title":"Automated Deduction in Geometry","author":"L.I. Meikle","year":"2006","unstructured":"Meikle, L.I., Fleuriot, J.D.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"6_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/11814771_4","volume-title":"Automated Reasoning","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 21\u201335. Springer, Heidelberg (2006)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing Convex Hull Algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 346\u2013361. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Geometry"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40672-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T21:02:05Z","timestamp":1558040525000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40672-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642406713","9783642406720"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40672-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}