A certified reduction strategy for homological image processing

DOI10.1145/2630789MaRDI QIDQ2946732zbMATH OpenOpenAlexFDO

Authors María Poza, César Domínguez, Jónathan Heras, Julio Rubio

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.0806

zbMATH Keywords

homologyCoqformalization of mathematicsbiomedical imagesSSReflectcomputational algebraic topology

Mathematics Subject Classification ID

Biomedical imaging and signal processing (92C55) Computing methodologies for image processing (68U10) Mechanization of proofs and logical operations (03B35) Chain complexes in algebraic topology (55U15)

Abstract: 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.

Recommendations

• Towards a certified computation of homology groups for digital images
• Verifying an algorithm computing discrete vector fields for digital imaging
• Paths, homotopy and reduction in digital images
• Computing persistent homology within Coq/SSReflect
• Reusing Integer Homology Information of Binary Digital Images

Cites work

• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 195162 (Why is no real title available?)
• A Fixed Point Approach to Homological Perturbation Theory
• A compiled implementation of strong reduction
• A mechanized proof of the basic perturbation lemma
• An introduction to small scale reflection in Coq
• Canonical Big Operators
• Combinatorial algebraic topology
• Computational topology. An introduction
• Computer Certified Efficient Exact Reals in Coq
• Computing persistent homology within Coq/SSReflect
• Constructive algebraic topology
• Effective homology of bicomplexes, formalized in Coq
• Extraction in Coq: An Overview
• Formal proof - the four color theorem
• Generating certified code from formal proofs: a case study in homological algebra
• Generating cubical complexes from image data and computation of the Euler number
• Homotopy in digital spaces
• Molecular shape analysis based upon the Morse-Smale complex and the Connolly function
• Morse theory for cell complexes
• Programming in Haskell

Cited in

(2)

• Towards a certified computation of homology groups for digital images
• Verifying an algorithm computing discrete vector fields for digital imaging

Describes a project that uses

Uses Software

• Coq/SSReflect
• QuickCheck
• Kenzo
• CoqEAL
• Haskell
• Coq

This page was built for publication: A certified reduction strategy for homological image processing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946732)