Generating certified code from formal proofs: a case study in homological algebra
scientific article; zbMATH DE number 5703857