Formal specification and proofs for the topology and classification of combinatorial surfaces
From MaRDI portal
Publication:396466
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
classificationformal specificationcomputational geometrygeometric modelingassisted proofcombinatorial surfacesCoq systemgeneralized mapssubdivisors
Uses Software
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
