Verifying an algorithm computing discrete vector fields for digital imaging

DOI10.1007/978-3-642-31374-5_15MaRDI QIDQ2907325zbMATH OpenOpenAlexFDO

Authors Jónathan Heras, María Poza, Julio Rubio

Publication date 7 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

Coqdiscrete vector fieldsHaskellintegrationSSReflect

Mathematics Subject Classification ID

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

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

Recommendations

• Towards a certified computation of homology groups for digital images
• A certified reduction strategy for homological image processing
• Computing persistent homology within Coq/SSReflect
• Effective homology of bicomplexes, formalized in Coq
• Incidence simplicial matrices formalized in Coq/SSReflect

Cited in

(2)

• Towards a certified computation of homology groups for digital images
• A certified reduction strategy for homological image processing

Describes a project that uses

Uses Software

• QuickCheck
• Kenzo
• Coq
• Coq/SSReflect

This page was built for publication: Verifying an algorithm computing discrete vector fields for digital imaging

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