C. [. Aransay, J. Ballarin, and . Rubio, A Mechanized Proof of the Basic Perturbation Lemma, Journal of Automated Reasoning, vol.126, issue.5, pp.271-292, 2008.
DOI : 10.1007/s10817-007-9094-x

E. [. Ayala, A. R. Domínguez, A. Francés, and . Quintero, Homotopy in digital spaces, Discrete Applied Mathematics, vol.125, issue.1, pp.3-24, 2003.
DOI : 10.1016/S0166-218X(02)00221-4

P. [. Bertot and . Castéran, Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

G. [. Bertot, S. O. Gonthier, I. Biha, and . Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics (TPHOLS'08), pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

C. Domínguez and J. Rubio, Effective homology of bicomplexes, formalized in Coq, Theoretical Computer Science, vol.412, issue.11
DOI : 10.1016/j.tcs.2010.11.016

X. Dousson, F. Sergeraert, and Y. Siret, The Kenzo program, Institut Fourier, 1998.

B. [. Gonzalez-diaz, P. Medrano, J. Real, and . Sanchez-pelaez, Algebraic Topological Analysis of Time-Sequence of Digital Images, Proceedings 8th International Conference on Computer Algebra in Scientific Computing (CASC'2005), pp.208-219, 2005.
DOI : 10.1007/11555964_18

P. [. Gonzalez-diaz, On the cohomology of 3D digital images, Discrete Applied Mathematics, vol.147, issue.2-3, pp.245-263, 2005.
DOI : 10.1016/j.dam.2004.09.014

A. [. Gonthier and . Mahboubi, A Small Scale Reflection Extension for the Coq system, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher-Order Logics (TPHOLS'07), pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

]. G. Gon08 and . Gonthier, Formal proof -The Four-Color Theorem, 2008.

M. [. Heras, M. Poza, L. Dénès, and . Rideau, Incidence Simplicial Matrices Formalized in Coq/SSReflect, 2010.
DOI : 10.1016/0097-3165(89)90053-8
URL : https://hal.archives-ouvertes.fr/inria-00603208

]. D. Mac03 and . Mackenzie, Topologists and Roboticists Explore and Inchoate World, Science, vol.8, p.756, 2003.

F. [. Orden and . Santos, Asymptotically Efficient Triangulations of the d -Cube, Discrete and Computational Geometry, vol.30, issue.4, pp.509-528, 2003.
DOI : 10.1007/s00454-003-2845-5

F. [. Rubio and . Sergeraert, Constructive Homological Algebra and Applications, Lecture Notes Summer School on Mathematics, Algorithms, and Proofs, 2006.

F. Ségonne, E. Grimson, and B. Fischl, Topological Correction of Subcortical Segmentation, Proceedings 6th International Conference on Medical Image Computing and Computer Assisted Intervention (MICCAI'2003), volume 2879 of Lecture Notes in Computer Science, pp.695-702, 2003.
DOI : 10.1007/978-3-540-39903-2_85

]. O. Veb31 and . Veblen, Analysis Situs, 1931.