{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:48:45Z","timestamp":1752230925884},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642302374"},{"type":"electronic","value":"9783642302381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30238-1_6","type":"book-chapter","created":{"date-parts":[[2012,6,12]],"date-time":"2012-06-12T07:19:22Z","timestamp":1339485562000},"page":"49-57","source":"Crossref","is-referenced-by-count":9,"title":["Towards a Certified Computation of Homology Groups for Digital Images"],"prefix":"10.1007","author":[{"given":"J\u00f3nathan","family":"Heras","sequence":"first","affiliation":[]},{"given":"Maxime","family":"D\u00e9n\u00e8s","sequence":"additional","affiliation":[]},{"given":"Gadea","family":"Mata","sequence":"additional","affiliation":[]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[]},{"given":"Mar\u00eda","family":"Poza","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"ForMath: formalisation of mathematics, \n                  \n                    http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ForMath\n                  \n                  \n                ."},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"M. Armand","year":"2010","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 83\u201398. Springer, Heidelberg (2010)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013360 (2003)","DOI":"10.1145\/777792.777845"},{"key":"6_CR4","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: Smith Normal form and executable rank for matrices, \n                  \n                    http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ProofExamples"},{"key":"6_CR5","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, version 8.3. Technical report (2010)"},{"issue":"8","key":"6_CR6","doi-asserted-by":"publisher","first-page":"2721","DOI":"10.1523\/JNEUROSCI.4477-10.2011","volume":"31","author":"G. Cuesto","year":"2011","unstructured":"Cuesto, G., et al.: Phosphoinositide-3-Kinase Activation Controls Synaptogenesis and Spinogenesis in Hippocampal Neurons. The Journal of Neuroscience\u00a031(8), 2721\u20132733 (2011)","journal-title":"The Journal of Neuroscience"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1006\/aima.1997.1650","volume":"134","author":"R. Forman","year":"1998","unstructured":"Forman, R.: Morse theory for cell complexes. Advances in Mathematics\u00a0134, 90\u2013145 (1998)","journal-title":"Advances in Mathematics"},{"key":"6_CR8","unstructured":"Gonthier, G.: Formal proof - The Four-Color Theorem, vol.\u00a055. Notices of the American Mathematical Society (2008)"},{"key":"6_CR9","unstructured":"Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Technical report, Microsoft Research INRIA (2009), \n                  \n                    http:\/\/hal.inria.fr\/inria-00258384"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/581478.581501","volume-title":"Proceedings of the Seventh ACM SIGPLAN international Conference on Functional Programming, ICFP 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, 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\u2013246. ACM, New York (2002)"},{"issue":"6","key":"6_CR11","doi-asserted-by":"publisher","first-page":"1619","DOI":"10.1109\/TVCG.2008.110","volume":"14","author":"A. Gyulassy","year":"2008","unstructured":"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\u00a014(6), 1619\u20131626 (2008)","journal-title":"IEEE Transactions on Visualization and Computer Graphics"},{"key":"6_CR12","unstructured":"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.\u00a01, pp. 41\u201347 (2010)"},{"key":"6_CR13","unstructured":"Heras, J., Mata, G., Poza, M., Rubio, J.: Homological processing of biomedical digital images: automation and certification. Technical report (2010), \n                  \n                    http:\/\/wiki.portal.chalmers.se\/cse\/uploads\/ForMath\/hpbdiac"},{"key":"6_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-22673-1_3","volume-title":"Intelligent Computer Mathematics","author":"J. Heras","year":"2011","unstructured":"Heras, J., Poza, M., D\u00e9n\u00e8s, 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.\u00a06824, pp. 30\u201344. Springer, Heidelberg (2011)"},{"key":"6_CR15","unstructured":"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.\u00a01, pp. 27\u201332 (2010)"},{"key":"6_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-22673-1_7","volume-title":"Intelligent Computer Mathematics","author":"R. Krebbers","year":"2011","unstructured":"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.\u00a06824, pp. 90\u2013106. Springer, Heidelberg (2011)"},{"key":"6_CR17","unstructured":"Mata, G.: SynapsCountJ. University of La Rioja (2011), \n                  \n                    http:\/\/imagejdocu.tudor.lu\/doku.php?id=plugin:utilities:synapsescountj:start"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-25379-9_26","volume-title":"Certified Programs and Proofs","author":"M. Boespflug","year":"2011","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full Reduction at Full Throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 362\u2013377. Springer, Heidelberg (2011)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-23672-3_6","volume-title":"Computer Analysis of Images and Patterns","author":"H. Molina-Abril","year":"2011","unstructured":"Molina-Abril, H., Real, P.: A Homological\u2013Based 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.\u00a06854, pp. 42\u201350. Springer, Heidelberg (2011)"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/j.patcog.2011.04.020","volume":"45","author":"M. Mrozek","year":"2012","unstructured":"Mrozek, M., et al.: Homological methods for extraction and analysis of linear features in multidimensional images. Pattern Recognition\u00a045(1), 285\u2013298 (2012)","journal-title":"Pattern Recognition"},{"key":"6_CR21","unstructured":"F.L.R.: node. From Digital Images to Simplicial Complexes: A report. Technical report (2011), \n                  \n                    http:\/\/wiki.portal.chalmers.se\/cse\/uploads\/ForMath\/fditscr"},{"key":"6_CR22","unstructured":"Rasband, W.S.: ImageJ: Image Processing and Analysis in Java (2003), \n                  \n                    http:\/\/rsb.info.nih.gov\/ij\/"},{"key":"6_CR23","unstructured":"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.\u00a01, pp. 33\u201340 (2010)"},{"issue":"8","key":"6_CR24","doi-asserted-by":"publisher","first-page":"1646","DOI":"10.1109\/TPAMI.2011.95","volume":"33","author":"V. Robins","year":"2011","unstructured":"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\u00a033(8), 1646\u20131658 (2011)","journal-title":"IEEE Transactions on Pattern Analysis and Machine Intelligence"},{"key":"6_CR25","unstructured":"Romero, A., Sergeraert, F.: Discrete Vector Fields and Fundamental Algebraic Topology (2010), \n                  \n                    http:\/\/arxiv.org\/abs\/1005.5685v1"},{"issue":"5594","key":"6_CR26","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1126\/science.1074069","volume":"298","author":"D.J. Selkoe","year":"2002","unstructured":"Selkoe, D.J.: Alzheimer\u2019s disease is a synaptic failure. Science\u00a0298(5594), 789\u2013791 (2002)","journal-title":"Science"},{"key":"6_CR27","doi-asserted-by":"publisher","first-page":"2833","DOI":"10.1016\/S0031-3203(01)00238-2","volume":"35","author":"D. Ziou","year":"2002","unstructured":"Ziou, D., Allili, M.: Generating Cubical Complexes from Image Data and Computation of the Euler number. Pattern Recognition\u00a035, 2833\u20132839 (2002)","journal-title":"Pattern Recognition"}],"container-title":["Lecture Notes in Computer Science","Computational Topology in Image Context"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30238-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T06:03:41Z","timestamp":1556863421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30238-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642302374","9783642302381"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30238-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}