Computing persistent homology within Coq/SSReflect

DOI10.1145/2528929zbMath1353.68251arXiv1209.1905OpenAlexW2021064762MaRDI QIDQ2946715

Vincent Siles, Jónathan Heras, Thierry Coquand, Anders Mörtberg

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/1209.1905

zbMATH Keywords

persistent homologyformalization of mathematicsCoqSSReflectcomputational algebraic topology

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other homology theories in algebraic topology (55N35)

Related Items (4)

Proof mining with dependent types ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Using abstract stobjs in ACL2 to compute matrix normal forms

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Computing persistent homology within Coq/SSReflect