A certified reduction strategy for homological image processing
The analysis of digital images using homological procedures is an outstanding topic
in the area of Computational Algebraic Topology. In this paper, we describe a certified
reduction strategy to deal with digital images, but preserving their homological
properties. We stress both the advantages of our approach (mainly, the formalisation 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.
You can download the code presented in the paper from here.
You can download the Haskell code from here.
You can see the theory graph of the different developments using the following links: