M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8

URL : https://hal.archives-ouvertes.fr/inria-00502496

F. Cazals, F. Chazal, and T. Lewiner, Molecular shape analysis based upon the morse-smale complex and the connolly function, Proceedings of the nineteenth conference on Computational geometry , SCG '03, pp.351-360, 2003.
DOI : 10.1145/777792.777845

C. Cohen, M. Dénès, A. Mörtberg, and V. Siles, Smith Normal form and executable rank for matrices

G. Cuesto, Phosphoinositide-3-Kinase Activation Controls Synaptogenesis and Spinogenesis in Hippocampal Neurons, Journal of Neuroscience, vol.31, issue.8, pp.312721-2733, 2011.
DOI : 10.1523/JNEUROSCI.4477-10.2011

R. Forman, Morse Theory for Cell Complexes, Advances in Mathematics, vol.134, issue.1, pp.90-145, 1998.
DOI : 10.1006/aima.1997.1650

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

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

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pp.235-246, 2002.

A. Gyulassy, P. Bremer, B. Hamann, and V. Pascucci, A Practical Approach to Morse-Smale Complex Computation: Scalability and Generality, IEEE Transactions on Visualization and Computer Graphics, vol.14, issue.6, pp.1619-1626, 2008.
DOI : 10.1109/TVCG.2008.110

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

S. Harker, The Efficiency of a Homology Algorithm based on Discrete Morse Theory and Coreductions, Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC'2010), volume 1 of Image A, pp.41-47, 2010.

J. Heras, G. Mata, M. Poza, and J. Rubio, Homological processing of biomedical digital images: automation and certification, 2010.

J. Heras, M. Poza, M. Dénès, and L. Rideau, Incidence Simplicial Matrices Formalized in Coq/SSReflect, Proceedings 18th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'2011), pp.30-44, 2011.
DOI : 10.1016/0097-3165(89)90053-8

URL : https://hal.archives-ouvertes.fr/inria-00603208

G. Jerse and N. M. Kosta, Tracking features in image sequences using discrete Morse functions, Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC'2010), volume 1 of Image A, pp.27-32, 2010.

R. Krebbers and B. Spitters, Computer Certified Efficient Exact Reals in Coq, pp.90-106, 2011.
DOI : 10.1007/978-3-642-04027-6_12

M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, Certified Programs and Proofs, pp.362-377, 2011.
DOI : 10.1007/3-540-44464-5_13

URL : https://hal.archives-ouvertes.fr/hal-00650940

H. Molina-abril and P. , A Homological???Based Description of Subdivided nD Objects, Proceedings of the 14th international conference on Computer analysis of images and patterns (CAIP'2011), pp.42-50, 2011.
DOI : 10.1007/978-3-642-23672-3_6

M. Mrozek, Homological methods for extraction and analysis of linear features in multidimensional images, Pattern Recognition, vol.45, issue.1, pp.285-298, 2012.
DOI : 10.1016/j.patcog.2011.04.020

F. L. Node, From Digital Images to Simplicial Complexes: A report, 2011.

W. S. Rasband, ImageJ: Image Processing and Analysis in Java, 2003.

P. Real and H. Molina, Towards Optimality in Discrete Morse Theory through Chain Homotopies, Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC'2010), volume 1 of Image A, pp.33-40, 2010.

V. Robins, P. Wood, and A. Sheppard, Theory and Algorithms for Constructing Discrete Morse Complexes from Grayscale Digital Images, IEEE Transactions on Pattern Analysis and Machine Intelligence, vol.33, issue.8, pp.1646-1658, 2011.
DOI : 10.1109/TPAMI.2011.95

A. Romero and F. Sergeraert, Discrete Vector Fields and Fundamental Algebraic Topology, 2010.

D. J. Selkoe, Alzheimer's Disease Is a Synaptic Failure, Science, vol.298, issue.5594, pp.298789-791, 2002.
DOI : 10.1126/science.1074069

D. Ziou and M. Allili, Generating cubical complexes from image data and computation of the Euler number, Pattern Recognition, vol.35, issue.12, pp.2833-2839, 2002.
DOI : 10.1016/S0031-3203(01)00238-2