{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T05:54:53Z","timestamp":1673070893178},"reference-count":44,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,3,1]],"date-time":"2000-03-01T00:00:00Z","timestamp":951868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4886,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,3]]},"DOI":"10.1016\/s0304-3975(98)00228-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T16:39:08Z","timestamp":1027615148000},"page":"1-57","source":"Crossref","is-referenced-by-count":9,"title":["Formalizing mathematics in higher-order logic: A case study in geometric modelling"],"prefix":"10.1016","volume":"234","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":"78","reference":[{"issue":"4","key":"10.1016\/S0304-3975(98)00228-X_BIB1","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1006\/gmip.1996.0028","article-title":"Jordan graphs","volume":"58","author":"Aharoni","year":"1996","journal-title":"Graphical Models Image Process."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(93)90303-B","article-title":"Classification des cartes point\u00e9es de genre 1 et relation fonctionnelle associ\u00e9e","volume":"117","author":"Arqu\u00e8s","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB3","series-title":"Graphes et Hypergraphes","author":"Berge","year":"1973"},{"issue":"7","key":"10.1016\/S0304-3975(98)00228-X_BIB4","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1007\/BF01177550","article-title":"Behavioural approaches to algebraic specifications: a comparative study","volume":"31","author":"Bernot","year":"1994","journal-title":"Acta Inform."},{"issue":"2","key":"10.1016\/S0304-3975(98)00228-X_BIB5","first-page":"161","article-title":"A generic approach to building user interfaces for theorem provers","volume":"25","author":"Bertot","year":"1998","journal-title":"JSC"},{"issue":"1","key":"10.1016\/S0304-3975(98)00228-X_BIB6","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1006\/cgip.1994.1005","article-title":"Algebraic specification of a 3D-modeler based on hypermaps","volume":"56","author":"Bertrand","year":"1994","journal-title":"Graphical Models Image Process."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB7","doi-asserted-by":"crossref","unstructured":"Y. Bertrand, J.-F. Dufourd, J. Fran\u00e7on, P. Lienhardt, Algebraic specification and development in geometric modeling, in TAPSOFT, Orsay, France, Lecture Notes in Computer Science, vol. 668, Springer, Berlin, 1993, pp. 74\u201387.","DOI":"10.1007\/3-540-56610-4_57"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB8","unstructured":"R. Butler et al., Nasa Langley's research and technology transfer program in formal methods, in COMPASS, Gaithersburg, MD, June 1995."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB9","unstructured":"G. Castagna, Surcharge, Sous-Typage et Liaison Tardive: Fondements Fonctionnels de la Programmation Orientee Objets, Ph.D. Thesis, LIENS, Paris 7, 1994."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB10","first-page":"605","article-title":"Term rewrite systems to derive set Boolean operations on 2D objects","volume":"vol. 1313","author":"Caziern","year":"1997"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB11","unstructured":"T. Coquand, Une Th\u00e9orie des Constructions, Ph.D. Thesis, Universit\u00e9 Paris 7, Paris, France, 1985."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB12","unstructured":"R. Cori, Un Code pour les Graphes Planaires et ses Applications, Soci\u00e9t\u00e9 Math. de France, Paris, Ast\u00e9risque 27, 1975."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB13","unstructured":"R. Cori, Cartes, Hypercartes et leurs Groupes d'Automorphismes, S\u00e9minaire Lotharingien de Combinatoire, Burg Fe\u00fcrstein, 1984, pp. 22\u201346."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB14","unstructured":"C. Cornes et al., The Coq Proof Assistant Reference Manual V6.1, INRIA-Rocquencourt, CNRS-ENS Lyon, France, December 1996."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB15","doi-asserted-by":"crossref","unstructured":"J.-F. Dufourd, An OBJ3 functional specification for boundary representation, Siggraph Symp. on Solid Modelling & CAD\/CAM Applications, Austin, USA, ACM Press, New York, 1991, pp. 61\u201372.","DOI":"10.1145\/112515.112529"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB16","unstructured":"J.-F. Dufourd, Foundations of boundary representation revisited with a new foremap axiomatics, Eurographics Internat. Workshop on Formal Specification in Computer Graphics, Marina di Carrara, Italy, 1991."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB17","doi-asserted-by":"crossref","unstructured":"J.-F. Dufourd, Algebras and formal specifications in geometric modeling, The Visual Computer, Springer, Berlin, 1997, pp. 131\u2013154.","DOI":"10.1007\/s003710050095"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB18","doi-asserted-by":"crossref","unstructured":"J.-F. Dufourd, P. Mathis et al., Formal resolution of geometrical constraint systems by assembling, ACM-Siggraph Solid Modeling, Atlanta, 1997, p. 271.","DOI":"10.1145\/267734.267804"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB19","unstructured":"J.-F. Dufourd, F. Puitg, Boundary representation specification revisited with a new Quasi-map concept, Graphical Models and Image Process. (1998), submitted."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB20","unstructured":"J. Fran\u00e7on, Topologie Combinatoire en Imagerie, Research Report 95\/12, Universit\u00e9 L. Pasteur, LSIIT, Strasbourg, France, 1995."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB21","unstructured":"L. Fuchs, D. Bechman, J.-F. Dufourd, Y. Bertrand, Formal specifications for free-form curves and surfaces, Computer Graphics Conf., Bratislava, 1996."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB22","series-title":"Introducing OBJ3, Applications of Algebraic Specifications Using OBJ","author":"Goguen","year":"1992"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB23","series-title":"Surfaces","author":"Griffiths","year":"1981"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB24","unstructured":"A. Jacques, Sur le Genre d'une Paire de Substitutions, Notes des membres et correspondants, vol. 267, 1968, pp. 625\u2013627."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB25","unstructured":"A. Jacques, Constellations et Graphes Topologiques, in: Combinatorial Theory and Applications, Budapest, Hungary, 1970, pp. 657\u2013673."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB26","first-page":"287","article-title":"An operational semantics of OBJ3","volume":"vol. 317","author":"Krichner","year":"1988"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB27","doi-asserted-by":"crossref","unstructured":"P. Lienhardt, Subdivisions of N-dimensional spaces and N-dimensional generalized maps, Computational Geometry ACM Symp., Saarbr\u00fccken, 1989, p. 228.","DOI":"10.1145\/73833.73859"},{"issue":"1","key":"10.1016\/S0304-3975(98)00228-X_BIB28","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0010-4485(91)90082-8","article-title":"Topological models for boundary representation. A survey","volume":"23","author":"Lienhardt","year":"1991","journal-title":"Comput. Aided Des."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB29","unstructured":"B. Liskov, S. Zilles, An introduction to formal specification methods, Current Trends in Programming Methodologie, vol. 1, Prentice-Hall, Englewood Cliffs, NJ, 1977, pp. 1\u201332."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB30","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Bibliopolis, Napels, 1984."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB31","unstructured":"C. Parent, Developing Certified Programs in the System Coq. The Program Tactic, Research Report 93-29, Ecole Normale Sup\u00e9rieure, Lyon, France, 1993."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB32","doi-asserted-by":"crossref","unstructured":"C. Parent, Synthesizing proofs from programs in the calculus of inductive constructions, Mathematics of Program Consturction, Lecture Notes in Computer Science, vol. 947, 1995, Springer, Berlin.","DOI":"10.1007\/3-540-60117-1_20"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB33","unstructured":"C. Paulin-Mohring, Inductive definitions in the system Coq \u2013 rules and properties, Typed Lambda-Calculi and Applications, Lecture Notes in Computer Science, vol. 664, 1993, Springer, Berlin."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB34","unstructured":"J.-P. Petit, Le Topologicon, Belin, 1985."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB35","unstructured":"F. Puitg, 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\/\u223cpuitg\/rr98\/main.html."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB36","doi-asserted-by":"crossref","unstructured":"F. Puitg, J.-F. Dufourd, Formal program development in geometric modelling, Current Trends in Applied Formal Methods, Boppard, Germany, Lecture Notes in Computer Science, Springer, Berlin, October 1998. http:\/\/dpt-info.u-strasbg.fr\/\u223cpuitg\/fmt98\/main.html.","DOI":"10.1007\/3-540-48257-1_3"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB37","doi-asserted-by":"crossref","unstructured":"F. Puitg, J.-F. Dufourd, Formal specifications and theorem proving breakthroughs in geometric modelling, in: Theorem Proving in Higher Order Logics, Canberra, Australia, Lecture Notes in Computer Science, Springer, Berlin, September 1998. http:\/\/dpt-info.u-strasbg. fr\/\u223cpuitg\/tpho198\/main.html.","DOI":"10.1007\/BFb0055149"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB38","unstructured":"F. Reinhardt, H. Soeder, Atlas des Math\u00e9matiques. Le livre de poche, 1997. French translation of the German \u201cAtlas zur Mathematik, 1974."},{"issue":"4","key":"10.1016\/S0304-3975(98)00228-X_BIB39","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1145\/356827.356833","article-title":"Representation for rigids solids","volume":"12","author":"Requicha","year":"1980","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB40","unstructured":"J. Rouyer, D\u00e9veloppements d'Algorithmes dans le Calcul des Constructions, Ph.D. Thesis, Institut National Polytechnique de Lorraine, Nancy, France, 1994."},{"issue":"2","key":"10.1016\/S0304-3975(98)00228-X_BIB41","doi-asserted-by":"crossref","first-page":"986","DOI":"10.4153\/CJM-1979-091-3","article-title":"Combinatorial oriented maps","volume":"XXXI","author":"Tutte","year":"1979","journal-title":"Can. J. Math."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB42","unstructured":"B. Werner, Une Th\u00e9orie des Constructions Inductives, Ph.D. Thesis, Universit\u00e9 Paris 7, Paris, France, 1994."},{"key":"10.1016\/S0304-3975(98)00228-X_BIB43","doi-asserted-by":"crossref","unstructured":"M. Wirsing, Algebraic specification, Formal Models and Semantics, Ch. 13, Elsevier, North-Holland, 1990, pp. 675\u2013788.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"10.1016\/S0304-3975(98)00228-X_BIB44","doi-asserted-by":"crossref","unstructured":"M. Yamamoto et al., Formalization of planar graphs, in: HOL Theorem Proving and its Applications, Aspen Grove, USA, Lecture Notes in Computer Science, vol. 971, Springer, Berlin, 1995, p. 369.","DOI":"10.1007\/3-540-60275-5_77"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439759800228X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439759800228X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T13:30:31Z","timestamp":1579181431000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439759800228X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,3]]},"references-count":44,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,3]]}},"alternative-id":["S030439759800228X"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(98)00228-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,3]]}}}