{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:57Z","timestamp":1725467517804},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055149","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"401-422","source":"Crossref","is-referenced-by-count":9,"title":["Formal specification and theorem proving breakthroughs in geometric modeling"],"prefix":"10.1007","author":[{"given":"Fran\u00c7ois","family":"Puitg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean -Fran\u00c7ois","family":"Dufourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"4","key":"24_CR1","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/gmip.1996.0028","volume":"58","author":"R. Aharoni","year":"1996","unstructured":"R. Aharoni, G. Herman, and M. Loebl. Jordan Graphs. Graphical Models and Image Processing, 58(4):345\u2013359, July 1996.","journal-title":"Graphical Models and Image Processing"},{"key":"24_CR2","volume-title":"Graphes et Hypergraphes","author":"C. Berge","year":"1973","unstructured":"C. Berge. Graphes et Hypergraphes. Dunod, Paris (France), 1973."},{"issue":"7","key":"24_CR3","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/BF01177550","volume":"31","author":"G. Bernot","year":"1994","unstructured":"G. Bernot, M. Bidoit, and T. Knapik. Behavioural Approaches to Algebraic Specifications: a Comparative Study. Acta Informatica 31(7):651\u2013671, 1994.","journal-title":"Acta Informatica"},{"issue":"1","key":"24_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1006\/gmip.1994.1005","volume":"56","author":"Y. Bertrand","year":"1994","unstructured":"Y. Bertrand and J.-F. Dufourd. Algebraic Specification of a 3D-Modeler Based on Hypermaps. Graphical Models and Image Processing, 56(1):29\u201360, 1994.","journal-title":"Graphical Models and Image Processing"},{"key":"24_CR5","first-page":"74","volume-title":"LNCS 668","author":"Y. Bertrand","year":"1993","unstructured":"Y. Bertrand, J.-F. Dufourd, J. Fran\u00c7on, and P. Lienhardt. Algebraic Specification and Development in Geometric Modeling. In TAPSOFT, pages 74\u201387, Orsay (France), 1993. Springer-Verlag, LNCS 668."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. Constructions: a Higher Order Proof System for Mechanizing Mathematics. In EUROCAL, Linz, 1985. LNCS 203.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"24_CR7","volume-title":"Ast\u00e9risque 27","author":"R. Cori","year":"1975","unstructured":"R. Cori. Un Code pour les Graphes Planaires et ses Applications. Soci\u00e9t\u00e9 Math. de France, Paris, Ast\u00e9risque 27, 1975."},{"key":"24_CR8","unstructured":"C. Cornes et al. The Coq Proof Assistant Reference Manual V6.1. INRIA-Rocquencourt, CNRS-ENS Lyon (France), December 1996."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"J.-F. Dufourd. Algebras and Formal Specifications in Geometric Modeling. In The Visual Computer, pages 131\u2013154. Spinger-Verlag, 1997.","DOI":"10.1007\/s003710050095"},{"key":"24_CR10","unstructured":"J.-F. Dufourd and F. Puitg. Boundary Representation Specification Revisited with a New Quasi-map Concept. Submitted to Graphical Models and Image Processing, 1998."},{"key":"24_CR11","volume-title":"Research report 95\/12","author":"J. Fran\u00c7on","year":"1995","unstructured":"J. Fran\u00c7on. Topologie Combinatoire en Imagerie. Research report 95\/12, Universit\u00e9 L. Pasteur, LSIIT, Strasbourg (France), 1995."},{"key":"24_CR12","unstructured":"H. Griffiths. Surfaces. Cambridge University Press, 1981."},{"key":"24_CR13","first-page":"625","volume":"267","author":"A. Jacques","year":"1968","unstructured":"A. Jacques. Sur le Genre d'une Paire de Substitutions. Notes des membres et correspondants, volume 267, pages 625\u2013627, 1968.","journal-title":"Notes des membres et correspondants"},{"key":"24_CR14","unstructured":"A. Jacques. Constellations et Graphes Topologiques. In Combinatorial Theory and Applications, pages 657\u2013673. Budapest (Hungary), 1970."},{"issue":"1","key":"24_CR15","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0010-4485(91)90082-8","volume":"23","author":"P. Lienhardt","year":"1991","unstructured":"P. Lienhardt. Topological Models for Boundary Representation: A Survey. In Computer Aided Design, volume 23(1), pages 59\u201381. 1991.","journal-title":"Computer Aided Design"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"C. Parent. Synthesizing Proofs from Programs in the Calculus of Inductive Constructions. In Mathematics of Program Construction. LNCS 947, 1995.","DOI":"10.1007\/3-540-60117-1_20"},{"key":"24_CR17","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq \u2014 Rules and Properties. In Typed Lambda-calculi and Applications. LNCS 664, 1993."},{"key":"24_CR18","unstructured":"J.-P. Petit. Le Topologicon. Belin, 1985."},{"key":"24_CR19","unstructured":"F. Puitg and J.-F. Dufourd. Sp\u00e9cifications en Mod\u00e9lisation G\u00e9om\u00e9trique par la Th\u00e9orie des Constructions. In Proc. Preuves et Sp\u00e9cifications Alg\u00e9briques, Grenoble (France), 1995. Journ\u00e9es du GDR de Programmation du CNRS."},{"key":"24_CR20","volume-title":"Tech. Rep. 98\/05","author":"F. Puitg","year":"1998","unstructured":"F. Puitg and J.-F. Dufourd. Combinatorial Maps and Planarity: Formal Specifications and Proofs in the Calculus of Inductive Constructions. Tech. Rep. 98\/05 (100 pages), LSIIT, Strasbourg (France). etsehttp:\/\/dpt-info.u-strasbg.fr\/~puitg\/rr98\/main.htmletse, 1998."},{"key":"24_CR21","volume-title":"PhD thesis","author":"J. Rouyer","year":"1994","unstructured":"J. Rouyer. D\u00e9veloppements d'Algorithmes dans le Calcul des Constructions. PhD thesis, Institut National Polytechnique de Lorraine, Nancy (France), March 1994."},{"issue":"2","key":"24_CR22","doi-asserted-by":"crossref","first-page":"986","DOI":"10.4153\/CJM-1979-091-3","volume":"XXXI","author":"W. Tutte","year":"1979","unstructured":"W. Tutte. Combinatorial Oriented Maps. In Canadian Journal of Mathematics, volume XXXI(2), pages 986\u20131004. 1979.","journal-title":"Canadian Journal of Mathematics"},{"key":"24_CR23","first-page":"675","volume-title":"Formal Models and Semantics","author":"M. Wirsing","year":"1990","unstructured":"M. Wirsing. Algebraic Specification. In Formal Models and Semantics, chapter 13, pages 675\u2013788. Elsevier, North-Holland, Amsterdam, 1990."},{"key":"24_CR24","series-title":"LNCS 971","first-page":"369","volume-title":"HOL Theorem Proving and Its Applications","author":"M. Yamamoto","year":"1995","unstructured":"M. Yamamoto et al. Formalization of Planar Graphs. In HOL Theorem Proving and Its Applications, p 369, Aspen Grove (USA), 1995. Springer-Verlag, LNCS 971."}],"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\/BFb0055149","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:32Z","timestamp":1555734872000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055149"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0055149","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}