eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2008-02-06
253
264
10.4230/LIPIcs.STACS.2008.1349
article
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Dufourd, Jean-Francois
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol001-stacs2008/LIPIcs.STACS.2008.1349/LIPIcs.STACS.2008.1349.pdf
Formal specifications
Computational topology
Computer-aided proofs
Coq
Planar subdivisions
Hypermaps
Jordan Curve Theorem