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