TY - RPRT TI - Computing Persistent Homology within Coq/SSReflect AU - Jónathan Heras AU - Thierry Coquand AU - Anders Mörtberg AU - Vincent Siles PY - 2012 UR - https://arxiv.org/abs/1209.1905 ID - 1209.1905 ER -