Aransay, Jesús; Ballarin, Clemens; Rubio, Julio Generating certified code from formal proofs: a case study in homological algebra. (English) Zbl 1214.68330 Formal Asp. Comput. 22, No. 2, 193-213 (2010). MSC: 68T15 18G35 68N30 PDFBibTeX XMLCite \textit{J. Aransay} et al., Formal Asp. Comput. 22, No. 2, 193--213 (2010; Zbl 1214.68330) Full Text: DOI HAL
Aransay, Jesús; Ballarin, Clemens; Rubio, Julio A mechanized proof of the basic perturbation lemma. (English) Zbl 1140.68059 J. Autom. Reasoning 40, No. 4, 271-292 (2008). MSC: 68T15 68W30 20K40 PDFBibTeX XMLCite \textit{J. Aransay} et al., J. Autom. Reasoning 40, No. 4, 271--292 (2008; Zbl 1140.68059) Full Text: DOI