Kenzo is a Computer Algebra System by Francis Sergeraert dealing with homologies and homotopies. The ongoing work I will expose aims at embedding a computer-certified version of it into the Coq proof-assistant. Which would give the tool both believable mathematical meaning and strong potency as a proof generating tool.

I will more specifically present a formalisation of categories which leads to a definition of homology. Not only do we need this formalisation to be mathematically relevant, i.e. to closely correspond to usual definitions of the manipulated concept, but we also need to program inside it. This emphasizes a few issues and solutions which can go beyond the original constructivity criterion.