Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps

Author Jean-Francois Dufourd

Thumbnail PDF


  • Filesize: 184 kB
  • 12 pages

Document Identifiers

Author Details

Jean-Francois Dufourd

Cite AsGet BibTex

Jean-Francois Dufourd. Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 253-264, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


This paper presents a formalized proof of a discrete form of the Jordan Curve Theorem. It is based on a hypermap model of planar subdivisions, formal specifications and proofs assisted by the Coq system. Fundamental properties are proven by structural or noetherian induction: Genus Theorem, Euler's Formula, constructive planarity criteria. A notion of ring of faces is inductively defined and a Jordan Curve Theorem is stated and proven for any planar hypermap.
  • Formal specifications
  • Computational topology
  • Computer-aided proofs
  • Coq
  • Planar subdivisions
  • Hypermaps
  • Jordan Curve Theorem


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads