A Certified Reduction Strategy for Homological Image Processing

DOI10.1145/2630789zbMath1354.68286arXiv1306.0806OpenAlexW1967904520MaRDI QIDQ2946732

Jónathan Heras, María Poza, César Domínguez, Julio Jesús Rubio García

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

homologyformalization of mathematicsCoqbiomedical imagesSSReflectcomputational algebraic topology

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Effective homology of bicomplexes, formalized in Coq
• A mechanized proof of the basic perturbation lemma
• Generating certified code from formal proofs: a case study in homological algebra
• Morse theory for cell complexes
• Constructive algebraic topology
• Generating cubical complexes from image data and computation of the Euler number
• Homotopy in digital spaces
• Computing persistent homology within Coq/SSReflect
• A compiled implementation of strong reduction
• Extraction in Coq: An Overview
• Canonical Big Operators
• A Fixed Point Approach to Homological Perturbation Theory
• Computer Certified Efficient Exact Reals in Coq
• Molecular shape analysis based upon the morse-smale complex and the connolly function
• Programming in Haskell
• Combinatorial algebraic topology