{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:18:44Z","timestamp":1750306724372,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,7,8]],"date-time":"2014-07-08T00:00:00Z","timestamp":1404777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Union's 7th Framework Programme","award":["243847"],"award-info":[{"award-number":["243847"]}]},{"name":"EPSRC","award":["EP\/J014222\/1 and EP\/K031864\/1"],"award-info":[{"award-number":["EP\/J014222\/1 and EP\/K031864\/1"]}]},{"name":"Ministerio de Educaci&#243;n y Ciencia project MTM2009-13842-C02-01"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,7,8]]},"abstract":"<jats:p>\n            The\n            <jats:italic>analysis of digital images<\/jats:italic>\n            using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this article, we describe a\n            <jats:italic>certified<\/jats:italic>\n            reduction strategy to deal with digital images, but one preserving their homological properties. We stress both the advantages of our approach (mainly, the formalization of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested.\n          <\/jats:p>","DOI":"10.1145\/2630789","type":"journal-article","created":{"date-parts":[[2014,7,22]],"date-time":"2014-07-22T15:08:20Z","timestamp":1406041700000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Certified Reduction Strategy for Homological Image Processing"],"prefix":"10.1145","volume":"15","author":[{"given":"Mar\u00eda","family":"Poza","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of La Rioja, Spain"}]},{"given":"C\u00e9sar","family":"Dom\u00ednguez","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University of La Rioja, Spain"}]},{"given":"J\u00f3nathan","family":"Heras","sequence":"additional","affiliation":[{"name":"School of Computing, University of Dundee, UK"}]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University of La Rioja, Spain"}]}],"member":"320","published-online":{"date-parts":[[2014,7,17]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/s10817-007-9094-x"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/s00165-009-0120-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-642-14052-5_8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1016\/S0166-218X(02)00221-4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1090\/S0002-9939-1991-1057939-0"},{"volume":"2410","volume-title":"Proceedings 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLS\u201902)","author":"Barthe G.","key":"e_1_2_1_6_1"},{"volume-title":"Neuroscience: Exploring the Brain","year":"2006","author":"Bear M.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"crossref","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer.   Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer.","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-662-07964-5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1007\/978-3-540-71067-7_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/978-3-642-25379-9_26"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/777792.777845"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/351240.351266"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1523\/JNEUROSCI.4477-10.2011"},{"volume-title":"Proceedings 3rd International Conference on Interactive Theorem Proving (ITP\u201912)","author":"D\u00e9n\u00e8s M.","key":"e_1_2_1_14_1"},{"unstructured":"M. D\u00e9n\u00e8s A. M\u00f6rtberg and V. Siles. 2013. CoqEAL the Coq Effective Algebra Library. (2013). Available at http:\/\/www.maximedenes.fr\/content\/coqeal-coq-effective-algebra-library.  M. D\u00e9n\u00e8s A. M\u00f6rtberg and V. Siles. 2013. CoqEAL the Coq Effective Algebra Library. (2013). Available at http:\/\/www.maximedenes.fr\/content\/coqeal-coq-effective-algebra-library.","key":"e_1_2_1_15_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1016\/j.tcs.2010.11.016"},{"unstructured":"X. Dousson J. Rubio F. Sergeraert and Y. Siret. 1998. The Kenzo program. Institut Fourier Grenoble. Available at http:\/\/www-fourier.ujf-grenoble.fr\/&sim;sergerar\/Kenzo\/.  X. Dousson J. Rubio F. Sergeraert and Y. Siret. 1998. The Kenzo program. Institut Fourier Grenoble. Available at http:\/\/www-fourier.ujf-grenoble.fr\/&sim;sergerar\/Kenzo\/.","key":"e_1_2_1_17_1"},{"volume-title":"Computational Topology: An Introduction","year":"2010","author":"Edelsbrunner H.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1006\/aima.1997.1650"},{"key":"e_1_2_1_20_1","first-page":"1382","article-title":"Formal proof - The Four-Color Theorem","volume":"55","author":"Gonthier G.","year":"2008","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_2_1_21_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier G.","year":"2010","journal-title":"Journal of Formal Reasoning"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/581478.581501"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1109\/TVCG.2008.110"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/978-3-642-30238-1_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1007\/978-3-642-31374-5_15"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/2528929"},{"key":"e_1_2_1_27_1","first-page":"29","article-title":"Homological processing of biomedical digital images: automation and certification","volume":"2","author":"Heras J.","year":"2011","journal-title":"Imagen-A"},{"doi-asserted-by":"crossref","unstructured":"G. Hutton. 2007. Programming in Haskell. Cambridge University Press.   G. Hutton. 2007. Programming in Haskell. Cambridge University Press.","key":"e_1_2_1_28_1","DOI":"10.1017\/CBO9780511813672"},{"unstructured":"N. Jacobson. 1989. Basic Algebra II. W. H. Freeman and Company.  N. Jacobson. 1989. Basic Algebra II. W. H. Freeman and Company.","key":"e_1_2_1_29_1"},{"volume":"1","volume-title":"Proceedings 3rd International Workshop on Computational Topology in Image Context (CTIC\u201910)","author":"Jerse G.","key":"e_1_2_1_30_1"},{"doi-asserted-by":"crossref","unstructured":"D. Kozlov. 2007. Combinatorial Algebraic Topology. Springer.  D. Kozlov. 2007. Combinatorial Algebraic Topology. Springer.","key":"e_1_2_1_31_1","DOI":"10.1007\/978-3-540-71962-5"},{"volume-title":"Proceedings Conferences Intelligent Computer Mathematics (CICM\u201911)","author":"Krebbers R.","key":"e_1_2_1_32_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1007\/978-3-540-69407-6_39"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1109\/TVCG.2004.18"},{"volume-title":"Mathematics, Algorithms and Proofs","year":"2010","author":"M\u00f6rtberg A.","key":"e_1_2_1_35_1"},{"unstructured":"A. Romero and F. Sergeraert. 2010. Discrete Vector Fields and Fundamental Algebraic Topology. Available at http:\/\/arxiv.org\/abs\/1005.5685v1.  A. Romero and F. Sergeraert. 2010. Discrete Vector Fields and Fundamental Algebraic Topology. Available at http:\/\/arxiv.org\/abs\/1005.5685v1.","key":"e_1_2_1_36_1"},{"unstructured":"A. Romero and F. Sergeraert. 2012. Homological Perturbation Theorem and Eilenberg-Zilber vector field. Available at http:\/\/www-fourier.ujf-grenoble.fr\/&sim;sergerar\/Talks\/12-06-Zurich-1.pdf.  A. Romero and F. Sergeraert. 2012. Homological Perturbation Theorem and Eilenberg-Zilber vector field. Available at http:\/\/www-fourier.ujf-grenoble.fr\/&sim;sergerar\/Talks\/12-06-Zurich-1.pdf.","key":"e_1_2_1_37_1"},{"unstructured":"J. Rubio and F. Sergeraert. 1997. Constructive Algebraic Topology Lecture Notes Summer School on Fundamental Algebraic Topology. Institut Fourier Grenoble. Available at http:\/\/www-fourier.ujf- grenoble.fr\/&sim;sergerar\/Summer-School\/.  J. Rubio and F. Sergeraert. 1997. Constructive Algebraic Topology Lecture Notes Summer School on Fundamental Algebraic Topology. Institut Fourier Grenoble. Available at http:\/\/www-fourier.ujf- grenoble.fr\/&sim;sergerar\/Summer-School\/.","key":"e_1_2_1_38_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1016\/S0007-4497(02)01119-3"},{"doi-asserted-by":"crossref","unstructured":"D. J. Selkoe. 2002. Alzheimer\u2019s disease is a synaptic failure. Science 298 5594 (2002) 789--791.  D. J. Selkoe. 2002. Alzheimer\u2019s disease is a synaptic failure. Science 298 5594 (2002) 789--791.","key":"e_1_2_1_40_1","DOI":"10.1126\/science.1074069"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1016\/S0031-3203(01)00238-2"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2630789","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2630789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:36Z","timestamp":1750231176000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2630789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,8]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,7,8]]}},"alternative-id":["10.1145\/2630789"],"URL":"https:\/\/doi.org\/10.1145\/2630789","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,7,8]]},"assertion":[{"value":"2013-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}