{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:18:00Z","timestamp":1725488280753},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_3","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T20:25:09Z","timestamp":1184963109000},"page":"62-76","source":"Crossref","is-referenced-by-count":2,"title":["Formal Program Development in Geometric Modeling"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Puitg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"J.A. Bergstra, J. Herig, et al. Algebraic Specification. ACM Press, 1988."},{"issue":"1","key":"3_CR2","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":"3_CR3","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":"3_CR4","doi-asserted-by":"crossref","unstructured":"J.A. Goguen et al. Introducing OBJ3. In Applications of Algebraic Specifications Using OBJ. Cambridge University Press, 1992.","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Puitg","year":"1998","unstructured":"F. Puitg and J.-F. Dufourd. Formal Specifications and Theorem Proving Breakthroughs in Geometric Modelling. In Theorem Proving in Higher Order Logics, Canberra (Australia), September 1998. Springer-Verlag, LNCS. http:\/\/dpt-info.u-strasbg.fr\/~puitg\/tphol98\/main.html ."},{"issue":"1","key":"3_CR6","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":"3_CR7","unstructured":"A. Jacques. Constellations et Graphes Topologiques. In Combinatorial Theory and Applications, pages 657\u2013673. Budapest (Hungary), 1970."},{"issue":"2","key":"3_CR8","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":"3_CR9","first-page":"625","volume":"267","author":"A. Jacques","year":"1968","unstructured":"A. Jacques. Sur le Genre d\u2019une Paire de Substitutions. Notes des membres et correspondants, volume 267, pages 625\u2013627, 1968.","journal-title":"Notes des membres et correspondants"},{"key":"3_CR10","unstructured":"R. Cori. Un Code pour les Graphes Planaires et ses Applications. Socit Math. de France, Paris, Ast\u00e9risque 27, 1975."},{"key":"3_CR11","series-title":"Tech. Rep.","volume-title":"Combinatorial Maps and Planarity: Formal Specifications and Proofs in the Calculus of Inductive Constructions","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), 1998. http:\/\/dpt-info.u-strasbg.fr\/~puitg\/rr98\/main.html ."},{"key":"3_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda-calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq \u2014 Rules and Properties. In Typed Lambda-calculi and Applications. LNCS 664, 1993."},{"key":"3_CR13","volume-title":"The Coq Proof Assistant Reference Manual V6.1","author":"C. Cornes","year":"1996","unstructured":"C. Cornes et al. The Coq Proof Assistant Reference Manual V6.1. INRIA-Rocquencourt, CNRS-ENS Lyon (France), December 1996."},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Mathematics of Program Construction","author":"C. Parent","year":"1995","unstructured":"C. Parent. Synthesizing Proofs from Programs in the Calculus of Inductive Constructions. In Mathematics of Program Construction. LNCS 947, 1995."}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T13:54:02Z","timestamp":1683986042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}