Computing persistent homology within Coq/SSReflect

DOI10.1145/2528929MaRDI QIDQ2946715zbMATH OpenOpenAlexFDO

Authors Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1209.1905

zbMATH Keywords

computational algebraic topologyCoqformalization of mathematicspersistent homologySSReflect

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other homology theories in algebraic topology (55N35)

Abstract: 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 paper, 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.

Recommendations

• Incidence simplicial matrices formalized in Coq/SSReflect
• On the role of formalization in computational mathematics
• Towards a certified computation of homology groups for digital images
• A Coq formalization of finitely presented modules
• Effective homology of bicomplexes, formalized in Coq

Cited in

(12)

• Using abstract stobjs in ACL2 to compute matrix normal forms
• Proof mining with dependent types
• A Coq formalization of finitely presented modules
• Towards a certified computation of homology groups for digital images
• Verifying an algorithm computing discrete vector fields for digital imaging
• A certified reduction strategy for homological image processing
• Formalization and execution of linear algebra: from theorems to algorithms
• Computing in Coq with infinite algebraic data structures
• On the role of formalization in computational mathematics
• Incidence simplicial matrices formalized in Coq/SSReflect
• Effective homology of bicomplexes, formalized in Coq
• Computational synthetic cohomology theory in homotopy type theory

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Computing persistent homology within Coq/SSReflect

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946715)