Formal specification and proofs for the topology and classification of combinatorial surfaces

DOI10.1016/j.comgeo.2014.04.007zbMath1296.65034OpenAlexW2030746297MaRDI QIDQ396466

Jean-François Dufourd, Christophe Dehlinger

Publication date: 13 August 2014

Published in: Computational Geometry (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.comgeo.2014.04.007

zbMATH Keywords

classificationformal specificationcomputational geometrygeometric modelingassisted proofcombinatorial surfacesCoq systemgeneralized mapssubdivisors

Mathematics Subject Classification ID

Numerical aspects of computer graphics, image analysis, and computational geometry (65D18)

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• A guide to the classification theorem for compact surfaces
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Formal specification of topological subdivisions using hypermaps
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
• Axioms and hulls
• Formalizing mathematics in higher-order logic: A case study in geometric modelling
• Functional specification and prototyping with oriented combinatorial maps
• Formalizing generalized maps in Coq
• Formalizing the trading theorem in Coq
• The axioms of constructive geometry
• Some topological properties of surfaces in \(Z^3\)
• FOUNDATIONS OF THE THEORY OF MAPS ON SURFACES WITH BOUNDARY
• N-DIMENSIONAL GENERALIZED COMBINATORIAL MAPS AND CELLULAR QUASI-MANIFOLDS
• Automated Deduction in Geometry
• Formal Study of Plane Delaunay Triangulation

This page was built for publication: Formal specification and proofs for the topology and classification of combinatorial surfaces