Abstract
In this paper we report on a project to obtain a verified computation of homology groups of digital images. The methodology is based on programming and executing inside the Coq proof assistant. Though more research is needed to integrate and make efficient more processing tools, we present some examples partially computed in Coq from real biomedical images.
Partially supported by Ministerio de Educación y Ciencia, project MTM2009-13842-C02-01, and by the European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath).
Chapter PDF
Similar content being viewed by others
References
ForMath: formalisation of mathematics, http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath .
Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 83–98. Springer, Heidelberg (2010)
Cazals, F., Chazal, F., Lewiner, T.: Molecular shape analysis based upon Morse-Smale complex and the Connolly function. In: Proceedings 19th ACM Symposium on Computational Geometry (SCG 2003), pp. 351–360 (2003)
Cohen, C., Dénès, M., Mörtberg, A., Siles, V.: Smith Normal form and executable rank for matrices, http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ProofExamples
Coq development team. The Coq Proof Assistant Reference Manual, version 8.3. Technical report (2010)
Cuesto, G., et al.: Phosphoinositide-3-Kinase Activation Controls Synaptogenesis and Spinogenesis in Hippocampal Neurons. The Journal of Neuroscience 31(8), 2721–2733 (2011)
Forman, R.: Morse theory for cell complexes. Advances in Mathematics 134, 90–145 (1998)
Gonthier, G.: Formal proof - The Four-Color Theorem, vol. 55. Notices of the American Mathematical Society (2008)
Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Technical report, Microsoft Research INRIA (2009), http://hal.inria.fr/inria-00258384
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of the Seventh ACM SIGPLAN international Conference on Functional Programming, ICFP 2002, pp. 235–246. ACM, New York (2002)
Gyulassy, A., Bremer, P., Hamann, B., Pascucci, V.: A practical approach to Morse-Smale complex computation: Scalability and generality. IEEE Transactions on Visualization and Computer Graphics 14(6), 1619–1626 (2008)
Harker, S., et al.: The Efficiency of a Homology Algorithm based on Discrete Morse Theory and Coreductions. In: Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC 2010). Image A, vol. 1, pp. 41–47 (2010)
Heras, J., Mata, G., Poza, M., Rubio, J.: Homological processing of biomedical digital images: automation and certification. Technical report (2010), http://wiki.portal.chalmers.se/cse/uploads/ForMath/hpbdiac
Heras, J., Poza, M., Dénès, M., Rideau, L.: Incidence Simplicial Matrices Formalized in Coq/SSReflect. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/ MKM 2011. LNCS (LNAI), vol. 6824, pp. 30–44. Springer, Heidelberg (2011)
Jerse, G., Kosta, N.M.: Tracking features in image sequences using discrete Morse functions. In: Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC 2010). Image A, vol. 1, pp. 27–32 (2010)
Krebbers, R., Spitters, B.: Computer Certified Efficient Exact Reals in Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 90–106. Springer, Heidelberg (2011)
Mata, G.: SynapsCountJ. University of La Rioja (2011), http://imagejdocu.tudor.lu/doku.php?id=plugin:utilities:synapsescountj:start
Boespflug, M., Dénès, M., Grégoire, B.: Full Reduction at Full Throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 362–377. Springer, Heidelberg (2011)
Molina-Abril, H., Real, P.: A Homological–Based Description of Subdivided nD Objects. In: Real, P., Diaz-Pernil, D., Molina-Abril, H., Berciano, A., Kropatsch, W. (eds.) CAIP 2011, Part I. LNCS, vol. 6854, pp. 42–50. Springer, Heidelberg (2011)
Mrozek, M., et al.: Homological methods for extraction and analysis of linear features in multidimensional images. Pattern Recognition 45(1), 285–298 (2012)
F.L.R.: node. From Digital Images to Simplicial Complexes: A report. Technical report (2011), http://wiki.portal.chalmers.se/cse/uploads/ForMath/fditscr
Rasband, W.S.: ImageJ: Image Processing and Analysis in Java (2003), http://rsb.info.nih.gov/ij/
Real, P., Molina-Abril, H.: Towards Optimality in Discrete Morse Theory through Chain Homotopies. In: Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC 2010). Image A, vol. 1, pp. 33–40 (2010)
Robins, V., Wood, P., Sheppard, A.: Theory and algorithms for constructing discrete Morse complexes from grayscale digital images. IEEE Transactions on Pattern Analysis and Machine Intelligence 33(8), 1646–1658 (2011)
Romero, A., Sergeraert, F.: Discrete Vector Fields and Fundamental Algebraic Topology (2010), http://arxiv.org/abs/1005.5685v1
Selkoe, D.J.: Alzheimer’s disease is a synaptic failure. Science 298(5594), 789–791 (2002)
Ziou, D., Allili, M.: Generating Cubical Complexes from Image Data and Computation of the Euler number. Pattern Recognition 35, 2833–2839 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heras, J., Dénès, M., Mata, G., Mörtberg, A., Poza, M., Siles, V. (2012). Towards a Certified Computation of Homology Groups for Digital Images. In: Ferri, M., Frosini, P., Landi, C., Cerri, A., Di Fabio, B. (eds) Computational Topology in Image Context. Lecture Notes in Computer Science, vol 7309. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30238-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-30238-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30237-4
Online ISBN: 978-3-642-30238-1
eBook Packages: Computer ScienceComputer Science (R0)