{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T17:58:21Z","timestamp":1769968701313,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,3,6]],"date-time":"2009-03-06T00:00:00Z","timestamp":1236297600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1007\/s10817-009-9117-x","type":"journal-article","created":{"date-parts":[[2009,3,5]],"date-time":"2009-03-05T08:33:09Z","timestamp":1236241989000},"page":"19-51","source":"Crossref","is-referenced-by-count":18,"title":["An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps"],"prefix":"10.1007","volume":"43","author":[{"given":"Jean-Fran\u00e7ois","family":"Dufourd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,6]]},"reference":[{"key":"9117_CR1","first-page":"67","volume-title":"Theorem Proving in HOL Conf. LNCS, vol. 2410","author":"G Bauer","year":"2002","unstructured":"Bauer, G., Nipkow, T.: The 5 colour theorem in Isabelle\/Isar. In: Theorem Proving in HOL Conf. LNCS, vol. 2410, pp. 67\u201382. Springer, New York (2002)"},{"key":"9117_CR2","volume-title":"Text in Theoretical Computer Science, An EATCS Series","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development\u2014Coq\u2019art: the calculus of inductive construction. In: Text in Theoretical Computer Science, An EATCS Series. Springer, New York (2004)"},{"key":"9117_CR3","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1006\/cgip.1994.1005","volume":"56","author":"Y Bertrand","year":"1994","unstructured":"Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graph. Models Image Process. 56, 1 29\u201360 (1994)","journal-title":"Graph. Models Image Process"},{"key":"9117_CR4","first-page":"82","volume-title":"SPIE Conf. on Vision Geometry VIII, vol. 3811","author":"L Chen","year":"1999","unstructured":"Chen, L.: Note on the discrete Jordan Curve Theorem. In: SPIE Conf. on Vision Geometry VIII, vol. 3811, pp. 82\u201394. SPIE, Bellingham (1999)"},{"key":"9117_CR5","unstructured":"The Coq Team Development-TypiCal Project: The Coq proof assistant reference manual\u2014version 8.1. INRIA, Le Chesnay http:\/\/coq.inria.fr\/doc-fra.html (2007)"},{"key":"9117_CR6","volume-title":"EUROCAL. LNCS, vol. 203","author":"T Coquand","year":"1985","unstructured":"Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. In: EUROCAL. LNCS, vol. 203. Springer, New York (1985)"},{"key":"9117_CR7","unstructured":"Cori, R.: Un code pour les graphes planaires et ses applications. Ast\u00e9risque 27 (1970) (Soci\u00e9t\u00e9 Math. de France)"},{"key":"9117_CR8","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1016\/j.tcs.2004.05.002","volume":"323","author":"C Dehlinger","year":"2004","unstructured":"Dehlinger, C., Dufourd, J.-F.: Formalizing the trading theorem in Coq. Theor. Comp. Sci. 323, 399\u2013442 (2004)","journal-title":"Theor. Comp. Sci."},{"key":"9117_CR9","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0925-7721(00)00004-3","volume":"16","author":"J-F Dufourd","year":"2000","unstructured":"Dufourd, J.-F., Puitg, F.: Functional specification and prototyping with combinatorial oriented maps. Comput. Geom. Theory Appl. 16, 129\u2013156 (2000)","journal-title":"Comput. Geom. Theory Appl."},{"key":"9117_CR10","doi-asserted-by":"crossref","first-page":"2974","DOI":"10.1016\/j.patcog.2007.02.013","volume":"40","author":"J-F Dufourd","year":"2007","unstructured":"Dufourd, J.-F.: Design and certification of a new optimal segmentation program with hypermaps. Pattern Recogn. 40, 2974\u20132993 (2007). doi: 10.101b\/j.patcog.2007.02.013","journal-title":"Pattern Recogn"},{"key":"9117_CR11","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/j.tcs.2008.02.012","volume":"403","author":"J-F Dufourd","year":"2008","unstructured":"Dufourd, J.-F.: Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof. Theor. Comp. Sci. 403, 133\u2013159 (2008). doi: 10.101b\/j.tcs.2008.02.012","journal-title":"Theor. Comp. Sci."},{"key":"9117_CR12","unstructured":"Dufourd, J.-F.: Discrete Jordan Curve Theorem: a proof formalized in Coq with hypermaps. In: Weil, P. (ed.) Symp. on Theoretical Aspects on Computer Science, 12 pp (2008). doi: hal-archives-ouvertes.fr\/hal-002211501~v1"},{"issue":"3","key":"9117_CR13","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1016\/j.scico.2006.10.002","volume":"24","author":"JC Filli\u00e2tre","year":"2006","unstructured":"Filli\u00e2tre, J.C.: Formal proof of a program: FIND. Sci. Comput. Program. 24(3), 332\u2013340 (2006)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"9117_CR14","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1006\/gmip.1995.1003","volume":"57","author":"J Fran\u00e7on","year":"1995","unstructured":"Fran\u00e7on, J.: Discrete combinatorial surfaces. CVGIP, Graph. Models Image Process. 57(1), 20\u201326 (1995)","journal-title":"CVGIP, Graph. Models Image Process."},{"key":"9117_CR15","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem, 57 pp. Microsoft Research, Cambridge. http:\/\/research.microsoft.com\/~gonthier (2005)"},{"key":"9117_CR16","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system, 75 pp. RR 6455, Microsoft Research-INRIA. http:\/\/hal.inria.fr\/inria-00258384\/ (2007)"},{"issue":"11","key":"9117_CR17","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof - the four-Colour theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"9117_CR18","volume-title":"Surfaces","author":"H Griffiths","year":"1981","unstructured":"Griffiths, H.: Surfaces. Cambridge University Press, Cambridge (1981)"},{"key":"9117_CR19","first-page":"117","volume-title":"Theorem Proving in HOL Conf. LNCS, vol. 3223","author":"T Hales","year":"2004","unstructured":"Hales, T.: Formalizing the proof of the Kepler conjecture. In: Theorem Proving in HOL Conf. LNCS, vol. 3223, p. 117. Springer, New York (2004)"},{"key":"9117_CR20","unstructured":"Hales, T.: A verified proof of the Jordan Curve Theorem. Seminar talk. Dep. of Math., University of Toronto http:\/\/www.math.pitt.edu\/~thales (2005)"},{"issue":"10","key":"9117_CR21","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"T Hales","year":"2007","unstructured":"Hales, T.: The Jordan Curve Theorem, formally and informally. Am. Math. Mon. 114(10), 882\u2013893 (2007)","journal-title":"Am. Math. Mon."},{"key":"9117_CR22","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant\u2014a tutorial\u2014version 8.0. Tech. report, INRIA, France http:\/\/coq.inria.fr\/doc-fra.html (2004)"},{"issue":"1","key":"9117_CR23","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/S0166-218X(02)00223-8","volume":"125","author":"M Khachan","year":"2003","unstructured":"Khachan, M., Chenin, P., Deddi, H.: Digital pseudomanifolds, digital weakmanifolds and Jordan-Brower separation theorem. Discrete Appl. Math. 125(1), 45\u201357 (2003)","journal-title":"Discrete Appl. Math."},{"issue":"4","key":"9117_CR24","first-page":"481","volume":"13","author":"A Kornilowicz","year":"2005","unstructured":"Kornilowicz, A.: Jordan Curve Theorem. Formaliz. Math. 13(4), 481\u2013491 (2005) (Univ. of Bialystock)","journal-title":"Formaliz. Math."},{"key":"9117_CR25","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/0734-189X(89)90147-3","volume":"48","author":"TY Kong","year":"1989","unstructured":"Kong, T.Y., Rosenfeld, A.: Digital topology: introduction and survey. Comput. Vis. Image Process. 48, 357\u2013393 (1989)","journal-title":"Comput. Vis. Image Process."},{"key":"9117_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(96)00213-7","volume":"186","author":"R Malgouyres","year":"1997","unstructured":"Malgouyres, R.: A definition of surfaces of Z3\u2014a new 3D discrete Jordan theorem. Theor. Comp. Sci. 186, 1\u201341 (1997)","journal-title":"Theor. Comp. Sci."},{"key":"9117_CR27","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda-Calculi and Applications. LNCS, vol. 664","author":"C Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definition in the system Coq\u2014rules and properties. In: Typed Lambda-Calculi and Applications. LNCS, vol. 664, pp. 328\u2013345. Springer, New York (1993)"},{"key":"9117_CR28","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1007\/s10817-006-9038-x","volume":"36","author":"C Simpson","year":"2006","unstructured":"Simpson, C.: Explaining Gabriel-Zisman localization to the computer. J. Autom. Reason. 36 (2006). doi: 10.1007\/s10817-006-9038-x,259\u2013285","journal-title":"J. Autom. Reason."},{"issue":"1\u20133","key":"9117_CR29","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/j.dam.2002.11.003","volume":"139","author":"J Slapal","year":"2004","unstructured":"Slapal, J.: A digital analog of the Jordan Curve Theorem. Discrete Appl. Math. 139(1\u20133), 231\u2013251 (2004)","journal-title":"Discrete Appl. Math."},{"key":"9117_CR30","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/0095-8956(83)90078-3","volume":"B 26","author":"S Stahl","year":"1983","unstructured":"Stahl, S.: A combinatorial analog of the Jordan Curve Theorem. J. Comb. Theory B 26, 28\u201338 (1983)","journal-title":"J. Comb. Theory"},{"issue":"5","key":"9117_CR31","doi-asserted-by":"crossref","first-page":"986","DOI":"10.4153\/CJM-1979-091-3","volume":"XXXI","author":"WT Tutte","year":"1979","unstructured":"Tutte, W.T.: Combinatorial oriented maps. Can. J. Math. XXXI(5), 986\u20131004 (1979)","journal-title":"Can. J. Math."},{"key":"9117_CR32","volume-title":"Encyclopedia of Mathematics and its Applications","author":"WT Tutte","year":"1984","unstructured":"Tutte, W.T.: Graph theory. In: Encyclopedia of Mathematics and its Applications. Addison Wesley, Reading (1984)"},{"key":"9117_CR33","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1090\/S0002-9947-1905-1500697-4","volume":"6","author":"O Veblen","year":"1905","unstructured":"Veblen, O.: Theory on plane curves in non-metrical analysis situs. Trans. Am. Math. Soc. 6, 83\u201398 (1905)","journal-title":"Trans. Am. Math. Soc."},{"key":"9117_CR34","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0095-8956(89)90027-0","volume":"B 47","author":"A Vince","year":"1989","unstructured":"Vince, A., Little, C.H.C.: Discrete Jordan Curve Theorems. J. Comb. Theory B 47, 251\u2013261 (1989)","journal-title":"J. Comb. Theory"},{"key":"9117_CR35","first-page":"369","volume-title":"Theorem Proving in HOL Conf. LNCS, vol. 971","author":"M Yamamoto","year":"1995","unstructured":"Yamamoto, M., Nishizaki, S., Hagiya, M., Tamai, T.: Formalization of planar graphs. In: Theorem Proving in HOL Conf. LNCS, vol. 971, pp. 369\u2013384. Springer, New York (1995)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9117-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9117-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9117-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9117-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,6]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["9117"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9117-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,6]]}}}