{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:22Z","timestamp":1725484282623},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_11","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"148-163","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing the Trading Theorem for the Classification of Surfaces"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Dehlinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"11_CR1","unstructured":"Barras, B. et al.: The Coq proof assistant reference manual. http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"11_CR2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1023\/A:1008348318797","volume":"11","author":"G. Bertrand","year":"1999","unstructured":"Bertrand, G., Malgouyres, R.: Some topological properties of surfaces in Z3. Journal of Mathematical Imaging and Vision no 11 (1999) 207\u2013221","journal-title":"Journal of Mathematical Imaging and Vision no"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1006\/gmip.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 (1994) 56(1) 29\u201360","journal-title":"Graphical Models and Image Processing"},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","volume-title":"EUROCAL","author":"T. Coquand","year":"1985","unstructured":"Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. EUROCAL (1985) Springer-Verlag LNCS 203"},{"key":"11_CR5","unstructured":"Cori, R.: Un Code pour les Graphes Planaires et ses Applications. Soci\u00e9t\u00e9 Math. de France, Ast\u00e9risque 27 (1970)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Dehlinger, C, Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hubert\u2019s Elementary Geometry. Automated Deduction in Geometry (2000) Springer-Verlag LNAI 2061","DOI":"10.1007\/3-540-45410-1_17"},{"key":"11_CR7","unstructured":"Firby, P. A., Gardiner, C. F.: Surface Topology. Ellis Horwood Ltd. (1982)"},{"key":"11_CR8","unstructured":"Fomenko, A. T.: Differential Geometry and Topology. Consultant Associates (1987)"},{"key":"11_CR9","unstructured":"Griffiths, H.: Surfaces. Cambridge University Press (1981)"},{"key":"11_CR10","unstructured":"Jacques, A.: Constellations et graphes topologiques. Combinatorial Theory And Applications (1970) 657\u2013673"},{"key":"11_CR11","unstructured":"Kahn, G.: Elements of Constructive Geometry, Group Theory, and Domain Theory. Coq contribution ( http:\/\/coq.inria.fr\/contribs-eng.html )"},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","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. Springer-Verlag (1992) LNCS 606"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Lienhardt, P.: Subdivisions of N-Dimensional Spaces and N-Dimensional Generalized Maps. Computational Geometry ACM Symp. (1989) 228\u2013236","DOI":"10.1145\/73833.73859"},{"key":"11_CR14","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis (1984)"},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Mathematics of Program Construction","author":"C. Parent","year":"1995","unstructured":"Parent, C: Synthesizing proofs from programs in the calculus of inductive constructions. Mathematics of Program Construction (1995) Springer-Verlag LNCS 947"},{"key":"11_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"TPHOL","author":"D. Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing Convex Hulls Algorithms. TPHOL (2001) Springer-Verlag LNCS 2152 346\u2013361"},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BFb0055149","volume-title":"TPHOL","author":"F. Puitg","year":"1998","unstructured":"Puitg, F., Dufourd, J.-F.: Formal specifications and theorem proving breakthroughs in geometric modelling. TPHOL (1998) Springer-Verlag LNCS 1479 401\u2013427"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0168-0072(95)00005-2","volume":"76","author":"J. Plato Von","year":"1995","unstructured":"Von Plato, J.: The axioms of constructive geometry. Annals of pure and applied logic 76 (1995) 169\u2013200","journal-title":"Annals of pure and applied logic"}],"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-45685-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:38:03Z","timestamp":1556429883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}