Computing persistent homology within coq/ssreflect

  1. Heras, J. 2
  2. Coquand, T. 13
  3. Mörtberg, A. 13
  4. Siles, Vincent . 13
  1. 1 Chalmers University of Technology
    info

    Chalmers University of Technology

    Gotemburgo, Suecia

    ROR https://ror.org/040wg7k59

  2. 2 University of Dundee
    info

    University of Dundee

    Dundee, Reino Unido

    ROR https://ror.org/03h2bxq36

  3. 3 University of Gothenburg
    info

    University of Gothenburg

    Gotemburgo, Suecia

    ROR https://ror.org/01tm6cn81

Mostrar afiliaciones +
Revista:
ACM Transactions on Computational Logic

ISSN: 1529-3785

Año de publicación: 2013

Volumen: 14

Número: 4

Tipo: Artículo

DOI: 10.1145/2528929 SCOPUS: 2-s2.0-84890420418 GOOGLE SCHOLAR

Otras publicaciones en: ACM Transactions on Computational Logic

Resumen

Persistent homology is one of the most active branches of computational algebraic topology 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 persistent Betti numbers, an instrumental tool of persistent homology, using the COQ proof assistant together with the SSREFLECT 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. © 2013 ACM 1529-3785/2013/11-ART25 $15.00.