Abstract | ||
---|---|---|
In this paper we report on a project to obtain a verified computation of homology groups of digital images. The methodology is based on programming and executing inside the Coq proof assistant. Though more research is needed to integrate and make efficient more processing tools, we present some examples partially computed in Coq from real biomedical images. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-30238-1_6 | CTIC |
Keywords | Field | DocType |
certified computation,digital image,homology group,coq proof assistant,processing tool,real biomedical image | Discrete mathematics,Singular homology,Computer science,Digital image,Theoretical computer science,Certification,Discrete Morse theory,Computation,Proof assistant | Conference |
Volume | ISSN | Citations |
7309 | 0302-9743 | 9 |
PageRank | References | Authors |
0.68 | 14 | 6 |
Name | Order | Citations | PageRank |
---|---|---|---|
Jónathan Heras | 1 | 94 | 23.31 |
Maxime Dénès | 2 | 64 | 4.91 |
Gadea Mata | 3 | 14 | 3.57 |
Anders Mörtberg | 4 | 59 | 5.44 |
María Poza | 5 | 20 | 2.29 |
Vincent Siles | 6 | 79 | 5.57 |