{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:39:05Z","timestamp":1752230345728,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>\n            <jats:italic>Persistent homology<\/jats:italic>\n            is one of the most active branches of\n            <jats:italic>computational algebraic topology<\/jats:italic>\n            with applications in several contexts such as optical character recognition or analysis of point cloud data. In this article, we report on the formal development of certified programs to compute\n            <jats:italic>persistent Betti numbers<\/jats:italic>\n            , an instrumental tool of persistent homology, using the C\n            <jats:sc>oq<\/jats:sc>\n            proof assistant together with the SSR\n            <jats:sc>eflect<\/jats:sc>\n            extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.\n          <\/jats:p>","DOI":"10.1145\/2528929","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T14:04:47Z","timestamp":1386165887000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Computing persistent homology within Coq\/SSReflect"],"prefix":"10.1145","volume":"14","author":[{"given":"J\u00f3nathan","family":"Heras","sequence":"first","affiliation":[{"name":"University of Dundee, UK"}]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology and University of Gothenburg, Sweden"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology and University of Gothenburg, Sweden"}]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology and University of Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2013,11,28]]},"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\/978-3-642-14052-5_8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-540-71067-7_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.5555\/3115437.3115553"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/1247069.1247105"},{"unstructured":"Chomp. 2013. Computational homology project. http:\/\/chomp.rutgers.edu\/software\/.  Chomp. 2013. Computational homology project. http:\/\/chomp.rutgers.edu\/software\/.","key":"e_1_2_1_6_1"},{"unstructured":"Coq Development Team. 2012. The coq proof assistant version 8.4. Tech. rep. http:\/\/flint.cs.yale.edu\/cs430\/coq\/pdf\/Reference-Manual.pdf.  Coq Development Team. 2012. The coq proof assistant version 8.4. Tech. rep. http:\/\/flint.cs.yale.edu\/cs430\/coq\/pdf\/Reference-Manual.pdf.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","first-page":"10","article-title":"Homological sensor networks","volume":"54","author":"De Silva V.","year":"2007","unstructured":"De Silva , V. and R. Ghrist , R. 2007 . Homological sensor networks . Notices Amer. Math. Soc. 54 , 1, 10 -- 17 . De Silva, V. and R. Ghrist, R. 2007. Homological sensor networks. Notices Amer. Math. Soc. 54, 1, 10--17.","journal-title":"Notices Amer. Math. Soc."},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/0167-8396(95)00016-Y"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1016\/j.comgeo.2005.10.006"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1016\/j.tcs.2010.11.016"},{"unstructured":"Dumas J. G. Heckenbach F. Saunders B. D. and Welker V. 2002. GAP homology package. http:\/\/www.linalg.org\/gap.html.  Dumas J. G. Heckenbach F. Saunders B. D. and Welker V. 2002. GAP homology package. http:\/\/www.linalg.org\/gap.html.","key":"e_1_2_1_12_1"},{"unstructured":"D\u00e9n\u00e8s M. M\u00f6rtberg A. and Siles. 2012a. CoqEAL the coq effective algebra library. http:\/\/www-sop.inria.fr\/members\/Maxime.Denes\/coqeal.  D\u00e9n\u00e8s M. M\u00f6rtberg A. and Siles. 2012a. CoqEAL the coq effective algebra library. http:\/\/www-sop.inria.fr\/members\/Maxime.Denes\/coqeal.","key":"e_1_2_1_13_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"e_1_2_1_15_1","volume-title":"Computational Topology: An Introduction","author":"Edelsbrunner H.","year":"2010","unstructured":"Edelsbrunner , H. and Harer , J. L . 2010 . Computational Topology: An Introduction . American Mathematical Society . Edelsbrunner, H. and Harer, J. L. 2010. Computational Topology: An Introduction. American Mathematical Society."},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/s00454-002-2885-2"},{"key":"e_1_2_1_17_1","first-page":"596","article-title":"Syze theory as a topological tool for computer vision","volume":"9","author":"Frosini P.","year":"1999","unstructured":"Frosini , P. and Landi , C. 1999 . Syze theory as a topological tool for computer vision . Pattern Recogn. Image Anal. 9 , 596 -- 603 . Frosini, P. and Landi, C. 1999. Syze theory as a topological tool for computer vision. Pattern Recogn. Image Anal. 9, 596--603.","journal-title":"Pattern Recogn. Image Anal."},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1090\/S0273-0979-07-01191-3"},{"key":"e_1_2_1_19_1","first-page":"1382","article-title":"Formal proof - The four-color theorem","volume":"55","author":"Gonthier G.","year":"2008","unstructured":"Gonthier , G. 2008 . Formal proof - The four-color theorem . Notices Amer. Math. Soc. 55 , 1382 -- 1394 . Gonthier, G. 2008. Formal proof - The four-color theorem. Notices Amer. Math. Soc. 55, 1382--1394.","journal-title":"Notices Amer. Math. Soc."},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.5555\/2033939.2033951"},{"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","unstructured":"Gonthier , G. and Mahboubi , A. 2010 . An introduction to small scale reflection in coq . J. Formal Reason. 3 , 2, 95 -- 152 . Gonthier, G. and Mahboubi, A. 2010. An introduction to small scale reflection in coq. J. Formal Reason. 3, 2, 95--152.","journal-title":"J. Formal Reason."},{"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.4007\/annals.2005.162.1065"},{"unstructured":"Hales. T. 2005b. The flyspeck project fact sheet. http:\/\/code.google.com\/p\/yspeck\/.  Hales. T. 2005b. The flyspeck project fact sheet. http:\/\/code.google.com\/p\/yspeck\/.","key":"e_1_2_1_24_1"},{"unstructured":"Heras J. Coquand T. Mortberg A. and Siles V. 2012a. Formalization of homology and persistent homology. http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ProofExamples.  Heras J. Coquand T. Mortberg A. and Siles V. 2012a. Formalization of homology and persistent homology. http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ProofExamples.","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1007\/978-3-642-30238-1_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.5555\/2032713.2032717"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/978-3-642-31374-5_15"},{"key":"e_1_2_1_29_1","volume-title":"Basic Algebra II","author":"Jacobson N.","unstructured":"Jacobson , N. 1989. Basic Algebra II 2 nd Ed. W. H. Freeman and Company . Jacobson, N. 1989. Basic Algebra II 2nd Ed. W. H. Freeman and Company.","edition":"2"},{"volume-title":"Persistent cubical homology in pattern recognition. Diplomarbeit","author":"Kedenburg G.","unstructured":"Kedenburg , G. 2010. Persistent cubical homology in pattern recognition. Diplomarbeit . University at Hamburg. Kedenburg, G. 2010. Persistent cubical homology in pattern recognition. Diplomarbeit. University at Hamburg.","key":"e_1_2_1_30_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1007\/978-3-642-25379-9_26"},{"doi-asserted-by":"crossref","unstructured":"Maclane S. 1963. Homology. Springer.  Maclane S. 1963. Homology. Springer.","key":"e_1_2_1_32_1","DOI":"10.1007\/978-3-642-62029-4"},{"unstructured":"Mathematical Components Team Homepage. 2013. http:\/\/www.msr-inria.inria.fr\/Projects\/math-components.  Mathematical Components Team Homepage. 2013. http:\/\/www.msr-inria.inria.fr\/Projects\/math-components.","key":"e_1_2_1_33_1"},{"unstructured":"Morozov D. 2012. Dionysus. http:\/\/www.mrzv.org\/software\/dionysus\/.  Morozov D. 2012. Dionysus. http:\/\/www.mrzv.org\/software\/dionysus\/.","key":"e_1_2_1_34_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1016\/j.patcog.2011.04.020"},{"key":"e_1_2_1_36_1","first-page":"969","article-title":"Analysis of blood vessel topology by cubical homology","volume":"2","author":"Niethammer M.","year":"2002","unstructured":"Niethammer , M. , Stein , A. N. , Kalies , W. D. , Pilarczyk , P. , Mischaikow , K. , and Tannenbaum , A. 2002 . Analysis of blood vessel topology by cubical homology . Image 2 , 2, 969 -- 972 . Niethammer, M., Stein, A. N., Kalies, W. D., Pilarczyk, P., Mischaikow, K., and Tannenbaum, A. 2002. Analysis of blood vessel topology by cubical homology. Image 2, 2, 969--972.","journal-title":"Image"},{"key":"e_1_2_1_37_1","first-page":"503","article-title":"Towards computing homology from finite approximations","volume":"24","author":"Robins V.","year":"1999","unstructured":"Robins , V. 1999 . Towards computing homology from finite approximations . Topology Proc. 24 , 503 -- 532 . Robins, V. 1999. Towards computing homology from finite approximations. Topology Proc. 24, 503--532.","journal-title":"Topology Proc."},{"unstructured":"Romero A. Heras J. Rubio J. and Sergeraert F. 2012. Defining and computing persistent z-homology in the general case. Tech. rep. http:\/\/staff.computing.dundee.ac.uk\/jheras\/papers.html.  Romero A. Heras J. Rubio J. and Sergeraert F. 2012. Defining and computing persistent z-homology in the general case. Tech. rep. http:\/\/staff.computing.dundee.ac.uk\/jheras\/papers.html.","key":"e_1_2_1_38_1"},{"unstructured":"Tausz A. Vejdemo-Johansson M. and Adams H. 2011. JavaPlex: A research software package for persistent (co)homology. http:\/\/code.google.com\/javaplex.  Tausz A. Vejdemo-Johansson M. and Adams H. 2011. JavaPlex: A research software package for persistent (co)homology. http:\/\/code.google.com\/javaplex.","key":"e_1_2_1_39_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1007\/s00454-004-1146-y"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2528929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:45Z","timestamp":1750231725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2528929"],"URL":"https:\/\/doi.org\/10.1145\/2528929","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}