@article{pershomology,
  author   = {Heras, J\'{o}nathan and Coquand, Thierry and M\"{o}rtberg, Anders and Siles, Vincent},
  title    = {{Computing Persistent Homology Within Coq/SSReflect}},
  keywords = {Coq, Persistent homology, SSReflect, computational algebraic topology, formalization of mathematics},
  journal  = {ACM Transactions on Computational Logic},
  year     = {2013},
  volume   = {14},
  number   = {4},
  pages    = {1-26},
  issn     = {1529-3785},
  doi      = {10.1145/2528929},
  url      = {http://doi.acm.org/10.1145/2528929},
}