Skip to Main content Skip to Navigation
Conference papers

Incidence simplicial matrices formalized in Coq/SSReflect

Abstract : Simplicial complexes are at the heart of Computational Algebraic Topology, since they give a concrete, combinatorial description of otherwise rather abstract objects which makes many important topological computations possible. The whole theory has many applications such as coding theory, robotics or digital image analysis. In this paper we present a formalization in the COQ theorem prover of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups and is a first step towards their computation.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download
Contributor : Maxime Dénès <>
Submitted on : Friday, June 24, 2011 - 2:18:35 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Sunday, September 25, 2011 - 2:23:18 AM


Files produced by the author(s)




Jónathan Heras, María Poza, Maxime Denes, Laurence Rideau. Incidence simplicial matrices formalized in Coq/SSReflect. Conference on Intelligent Computer Mathematics, Jul 2011, Bertinoro, Italy. ⟨10.1007/978-3-642-22673-1_3⟩. ⟨inria-00603208⟩



Record views


Files downloads