Name
Abstract | ||
|---|---|---|
The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this article, we describe a certified 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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2630789 | ACM Trans. Comput. Log. |
Keywords | DocType | Volume |
formalization of mathematics,ssreflect,verification,homology,mechanical theorem proving,computational algebraic topology,reliability,biomedical images,formal methods,coq | Journal | 15 |
Issue | ISSN | Citations |
3 | ACM Transactions on Computational Logic, Volume 15 Issue 3,
Article No. 23 2014 | 2 |
PageRank | References | Authors |
0.41 | 20 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| María Poza | 1 | 20 | 2.29 |
| César Domínguez | 2 | 95 | 18.93 |
| Jónathan Heras | 3 | 94 | 23.31 |
| J. Rubio | 4 | 202 | 31.12 |