{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T18:38:55Z","timestamp":1760121535554},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"},{"type":"electronic","value":"9783540447559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_24","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:03:32Z","timestamp":1186740212000},"page":"346-361","source":"Crossref","is-referenced-by-count":22,"title":["Formalizing Convex Hull Algorithms"],"prefix":"10.1007","author":[{"given":"David","family":"Pichardie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yves","family":"Bertot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1023\/A:1009942427413","volume":"6","author":"P. Alliez","year":"2000","unstructured":"Pierre Alliez, Olivier Devillers, and Jack Snoeyink. Removing degeneracies by perturbing the problem or the world. Reliable Computing, 6:61\u201379, 2000. Special Issue on Computational Geometry.","journal-title":"Reliable Computing"},{"key":"24_CR2","unstructured":"Bruno Barras, Samuel Boutin, Cristina Cornes, Judicael Courant, Yann Coscoy, David Delahaye, Jean-Christophe Filliatre Daniel de Rauglaudre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant User\u2019s Guide. Version 6.3.1. INRIA, December 1999."},{"key":"24_CR3","unstructured":"Jean-Daniel Boissonnat and Mariette Yvinec. Algorithmic geometry. Cambridge University Press, 1995."},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Science","author":"S. Boutin","year":"1997","unstructured":"Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Theoretical Aspects of Computer Science, number 1281 in Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"24_CR5","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry","author":"S.C. Chou","year":"1994","unstructured":"S.C. Chou, X.S. Gao, and J.Z. Zhang. Machine Proofs in Geometry. World Scientific, Singapore, 1994."},{"key":"24_CR6","unstructured":"Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to algorithms. MIT-Press, 1990."},{"key":"24_CR7","unstructured":"Gilles Kahn. Elements of constructive geometry group theory and domain theory, 1995. Available as a Coq contribution at \n                    http:\/\/coq.inria.fr\/contribs-eng.html\n                    \n                  ."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Axioms and Hulls","author":"D. Knuth","year":"1991","unstructured":"Donald Knuth. Axioms and Hulls. Number 606 in Lecture Notes in Computer Science. Springer-Verlag, 1991."},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/BFb0055149","volume-title":"Theorem Proving in Higher-Order Logics","author":"F. Puitg","year":"1998","unstructured":"Fran\u00e7ois Puitg and Jean-Fran\u00e7ois Dufourd. Formal specification and theorem proving breakthroughs in geometric modeling. In Theorem Proving in Higher-Order Logics, volume 1479 of Lecture Notes in Computer Science, pages 410\u2013422. Springer-Verlag, 1998."},{"key":"24_CR10","unstructured":"Robert Sedgewick. Algorithms. Addison-Wesley, 1988."},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1016\/S0019-3577(98)80034-7","volume":"9","author":"J. Plato von","year":"1998","unstructured":"Jan von Plato. A constructive theory of ordered affine geometry. Indagationes Mathematicae, 9:549\u2013562, 1998.","journal-title":"Indagationes Mathematicae"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T12:00:33Z","timestamp":1550750433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}