{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:26Z","timestamp":1748413526475,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_16","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"211-226","source":"Crossref","is-referenced-by-count":12,"title":["Formal Study of Plane Delaunay Triangulation"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yves","family":"Bertot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45685-6_6","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bauer","year":"2002","unstructured":"Bauer, G., Nipkow, T.: The 5 Colour Theorem in Isabelle\/Isar. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 67\u201382. Springer, Heidelberg (2002)"},{"key":"16_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-77974-2","volume-title":"Computational Geometry: Algorithms and Applications","author":"M. de Berg","year":"2008","unstructured":"de Berg, M., Cheong, O., van Kreveld, M., Overmars, M.: Computational Geometry: Algorithms and Applications, 3rd edn. Springer, Heidelberg (2008)","edition":"3"},{"issue":"1","key":"16_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1006\/cgip.1994.1005","volume":"56","author":"Y. Bertrand","year":"1994","unstructured":"Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graphical Models and Image Processing\u00a056(1), 29\u201360 (1994)","journal-title":"Graphical Models and Image Processing"},{"key":"16_CR4","series-title":"An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions, Text in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions, Text in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"16_CR5","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, 225\u2013252 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F. Besson","year":"2007","unstructured":"Besson, F.: Fast Reflexive Arithmetic Tactics: the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 48\u201362. Springer, Heidelberg (2007)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Boissonnat, J.-D., Devillers, O., Pion, S., Teillaud, M., Yvinec, M.: Tiangulations in CGAL. Comp. Geom. - Th and Appl.\u00a022(1-3), 5\u20139 (2002); Spec. iss. SOCG\u201900 (2002)","DOI":"10.1016\/S0925-7721(01)00054-2"},{"key":"16_CR8","unstructured":"Brun, C., Dufourd, J.-F., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. (submitted 2009)"},{"key":"16_CR9","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual - Version 8.2. INRIA, France (2009), \n                      http:\/\/coq.inria.fr"},{"key":"16_CR10","unstructured":"Cori, R.: Un Code pour les Graphes Planaires et ses Applications. Ast\u00e9risque\u00a027 (1970); Soci\u00e9t\u00e9 Math. de France"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/j.tcs.2004.05.002","volume":"323","author":"C. Dehlinger","year":"2004","unstructured":"Dehlinger, C., Dufourd, J.-F.: Formalizing the trading theorem in Coq. Theoretical Computer Science\u00a0323, 399\u2013442 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0925-7721(00)00004-3","volume":"16","author":"J.-F. Dufourd","year":"2000","unstructured":"Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial oriented maps. Comp. Geometry - Th. and Appl.\u00a016(2), 129\u2013156 (2000)","journal-title":"Comp. Geometry - Th. and Appl."},{"key":"16_CR13","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, 2974\u20132993 (2007)","journal-title":"Pattern Recognition"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.tcs.2008.02.012","volume":"403","author":"J.-F. Dufourd","year":"2008","unstructured":"Dufourd, J.-F.: Polyhedra genus theorem and Euler Formula: A hypermap-formalized intuitionistic proof. Theor. Comp. Sc.\u00a0403, 133\u2013159 (2008)","journal-title":"Theor. Comp. Sc."},{"key":"16_CR15","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 Theorem Formalized in Coq with Hypermaps. Journal of Automated Reasoning\u00a043, 19\u201351 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR16","unstructured":"Dufourd, J.-F.: Reasoning formally with Split, Merge and Flip in plane triangulations (submitted 2009), \n                      http:\/\/lsiit.u-strasbg.fr\/Publications\/index.php"},{"key":"16_CR17","unstructured":"Dufourd, J.-F., Bertot, Y.: Formal proof of Delaunay by edge flipping (2010), \n                      http:\/\/galapagos.gforge.inria.fr\/devel\/DelaunayFlip.tgz"},{"key":"16_CR18","first-page":"1","volume-title":"Acta Numerica","author":"H. Edelsbrunner","year":"2000","unstructured":"Edelsbrunner, H.: Triangulations and meshes in combinatorial geometry. In: Acta Numerica, pp. 1\u201381. Cambridge Univ. Press, Cambridge (2000)"},{"key":"16_CR19","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., et al.: The Design and Implementation of Planar Maps in CGAL. WAE 1999\u00a016 (2000); In: Vitter, J.S., Zaroliagis, C.D. (eds.) WAE 1999. LNCS, vol.\u00a01668, pp. 154\u2013168. Springer, Heidelberg (1999)"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Fousse, L., et al.: MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw.\u00a033(2) (2007)","DOI":"10.1145\/1236463.1236468"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"16_CR22","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof - the four-Colour theorem. Not. Am. Math. Soc.\u00a055, 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"2","key":"16_CR23","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/282918.282923","volume":"4","author":"L. Guibas","year":"1985","unstructured":"Guibas, L., Stolfi, J.: Primitives for the Manipulation of General Subdivisions and the Computation of Voronoi Diagrams. ACM TOG\u00a04(2), 74\u2013123 (1985)","journal-title":"ACM TOG"},{"key":"16_CR24","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.comgeo.2007.06.003","volume":"40","author":"L. Kettener","year":"2008","unstructured":"Kettener, L., Mehlhorn, K., Pion, S., Scirra, S., Yap, C.: Classroom examples of robustness problems in geometric computations. Computational Geometry - Theory and Applications\u00a040, 61\u201378 (2008)","journal-title":"Computational Geometry - Theory and Applications"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"16_CR26","series-title":"Lecture Notes in Artificial Intelligence","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.: Mechanical Theorem Proving in Computational Geometry. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol.\u00a03763, pp. 1\u201318. Springer, Heidelberg (2006)"},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1051\/ita:2007005","volume":"41","author":"G. Melquiond","year":"2007","unstructured":"Melquiond, G., Pion, S.: Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates. Theoretical Informatics and Applications, EDP Science\u00a041(1), 57\u201369 (2007)","journal-title":"Theoretical Informatics and Applications, EDP Science"},{"issue":"3-4","key":"16_CR28","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10472-009-9168-z","volume":"56","author":"S. Obua","year":"2009","unstructured":"Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Annals of Mathematics and Artificial Intelligence\u00a056(3-4), 245\u2013272 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"16_CR29","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 Hulls Algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 346\u2013361. Springer, Heidelberg (2001)"},{"key":"16_CR30","first-page":"132","volume-title":"Tenth Symposium on Computer Arithmetic","author":"D. Priest","year":"1991","unstructured":"Priest, D.: Algorithms for Arbitrary Precision Floating Point Arithmetic. In: Tenth Symposium on Computer Arithmetic, pp. 132\u2013143. IEEE, Los Alamitos (1991)"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0055149","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Puitg","year":"1998","unstructured":"Puitg, F., Dufourd, J.-F.: Formal specifications and theorem proving breakthroughs in geometric modelling. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 401\u2013427. Springer, Heidelberg (1998)"},{"key":"16_CR32","volume-title":"Graph Theory. Encyclopedia of Mathematics and its Applications","author":"W.E. Tutte","year":"1984","unstructured":"Tutte, W.E.: Graph Theory. Encyclopedia of Mathematics and its Applications. Addison Wesley, Reading (1984)"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Yap, C.-K., Pion, S.: Special Issue on Robust Geometric Algorithms and their Implementations. Computational Geometry - Theory and Applications\u00a033(1-2) (2006)","DOI":"10.1016\/j.comgeo.2005.08.001"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:27:12Z","timestamp":1676690832000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}