Name
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 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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2528929 | ACM Transactions on Computational Logic (TOCL) |
Keywords | DocType | Volume |
computing persistent homology,nontrivial mathematical theory,certified program,active branch,underlying mathematical theory,persistent betti number,persistent homology,ssreflect extension,computational algebraic topology,point cloud data,coq proof assistant | Journal | 14 |
Issue | ISSN | Citations |
4 | 1529-3785 | 8 |
PageRank | References | Authors |
0.53 | 17 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jónathan Heras | 1 | 94 | 23.31 |
| Thierry Coquand | 2 | 1537 | 225.49 |
| Anders Mörtberg | 3 | 59 | 5.44 |
| Vincent Siles | 4 | 79 | 5.57 |