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

Jean-François Dufourd

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 assi…