Verifying an algorithm computing Discrete Vector Fields for digital imaging
This work addresses the problem of efficiently analyzing homological properties in digital biomedical images for researchers in computational topology and medical imaging, though it is incremental as it builds on existing discrete vector field methods.
The authors formalized an algorithm for constructing admissible discrete vector fields in Coq using the SSReflect library, enabling the computation of homological properties of biomedical images that were previously infeasible in this system.
In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discrete vector fields are a tool which has been welcomed in the homological analysis of digital images since it provides a procedure to reduce the amount of information but preserving the homological properties. In particular, thanks to discrete vector fields, we are able to compute, inside Coq, homological properties of biomedical images which otherwise are out of the reach of this system.