Formalizing generalized maps in Coq

DOI10.1016/j.tcs.2004.05.003zbMath1078.68136OpenAlexW2001300597MaRDI QIDQ1882905

Jean-François Dufourd, Christophe Dehlinger

Publication date: 1 October 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.05.003

zbMATH Keywords

SpecificationCoqSurfacesProofGeometry modellingCalculus of Inductive ConstructionsGeneralized maps

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Related Items

Formal specification and proofs for the topology and classification of combinatorial surfaces, Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof, Formalization of the Poincaré disc model of hyperbolic geometry, Coq

Cites Work

• Axioms and hulls
• The axioms of constructive geometry
• Some topological properties of surfaces in \(Z^3\)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item