License: 
Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2008.1349
URN: urn:nbn:de:0030-drops-13493
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1349/
Dufourd, Jean-Francois
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Abstract
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.
BibTeX - Entry
@InProceedings{dufourd:LIPIcs:2008:1349,
author = {Jean-Francois Dufourd},
title = {{Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps}},
booktitle = {25th International Symposium on Theoretical Aspects of Computer Science},
pages = {253--264},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-06-4},
ISSN = {1868-8969},
year = {2008},
volume = {1},
editor = {Susanne Albers and Pascal Weil},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1349},
URN = {urn:nbn:de:0030-drops-13493},
doi = {10.4230/LIPIcs.STACS.2008.1349},
annote = {Keywords: Formal specifications, Computational topology, Computer-aided proofs, Coq, Planar subdivisions, Hypermaps, Jordan Curve Theorem}
}
|
Keywords: |
|
Formal specifications, Computational topology, Computer-aided proofs, Coq, Planar subdivisions, Hypermaps, Jordan Curve Theorem |
|
Collection: |
|
25th International Symposium on Theoretical Aspects of Computer Science |
|
Issue Date: |
|
2008 |
|
Date of publication: |
|
06.02.2008 |
