Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (CPP, 2012)

Coquelicot: A User-Friendly Library of Real Analysis for Coq. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Comput. Sci., 2015)

Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. (Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis). - Catherine Lelay (2015)

Formalization of real analysis: a survey of proof assistants and libraries. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Struct. Comput. Sci., 2016)