Formalizing the trading theorem in Coq

DOI10.1016/j.tcs.2004.05.002zbMath1078.68137OpenAlexW1987816136MaRDI QIDQ1882906

Christophe Dehlinger, Jean-François Dufourd

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.002

zbMATH Keywords

SpecificationCoqSurfacesGeometry modellingCalculus of Inductive ConstructionsGeneralized maps

Mathematics Subject Classification ID

Computational aspects related to convexity (52B55) Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Related Items

An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps, Design and formal proof of a new optimal image segmentation program with hypermaps, Formal specification and proofs for the topology and classification of combinatorial surfaces, Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

Uses Software

• Coq

Cites Work

• Some topological properties of surfaces in \(Z^3\)
• Combinatorial Oriented Maps
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item