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

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.

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Jean-François Dufourd
• Keywords: Constructive Planarity Criteria, CORR 2008, Education, Formalized Proof, Jordan Curve Theorem