Towards a Certified Computation of Homology Groups for Digital Images

DOI10.1007/978-3-642-30238-1_6zbMath1357.68280OpenAlexW2151373060MaRDI QIDQ2900562

Maxime Dénès, Gadea Mata, Anders Mörtberg, Jónathan Heras, María Poza, Vincent Siles

Publication date: 23 July 2012

Published in: Computational Topology in Image Context (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-30238-1_6

zbMATH Keywords

homologydiscrete Morse theoryCoqsynapsesSSReflectproof assistant tools

Mathematics Subject Classification ID

Computing methodologies for image processing (68U10) Biomedical imaging and signal processing (92C55)

Related Items (2)

Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

Uses Software

• Coq
• Coq/SSReflect
• ImageJ
• SynapsCountJ

This page was built for publication: Towards a Certified Computation of Homology Groups for Digital Images