We describe one of the first attempts at using modern specification techniques in the field of geometric modelling and computational geometry. Using the Coq system, we developed a formal multi-level specification of combinatorial maps, used to represent subdivisions of geometric manifolds, and then exploited it to formally prove fundamental theorems. In particular, we outline here an original and constructive proof of a combinatorial part of the famous Surface Classification Theorem, based on a set of so-called ``conservative'' elementary operations on subdivisions.

C. Dehlinger , J-F. Dufourd

Computational Geometry : Theory and Applications , Volume 47 , Number 9 , page 869--890 - 2014

Additionnal material

International journal
Formal specification and proofs for the topology and classification of combinatorial surfaces, * Computational Geometry : Theory and Applications*, Elsevier ( IF : 0.476 ), pages 869--890, Volume 47, n° 9, octobre 2014, *doi:10.1016/j.comgeo.2014.04.007*
__Research team__ : IGG

@Article{2-DD14, author = {Dehlinger, C. and Dufourd, J-F.}, title = {Formal specification and proofs for the topology and classification of combinatorial surfaces}, journal = {Computational Geometry : Theory and Applications}, number = {9}, volume = {47}, pages = {869--890}, month = {Oct}, year = {2014}, doi = {10.1016/j.comgeo.2014.04.007}, x-international-audience = {Yes}, x-language = {EN}, url = {http://icube-publis.unistra.fr/2-DD14} }

See publications of the same authors