[. Bertot and P. Castéran, Gérard (informaticien) Huet, and Christine Paulin-Mohring. Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions. Texts in theoretical computer science, 2004.

S. Boldo, J. Jourdan, X. Leroy, and G. Melquiond, A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.107-115, 2013.
DOI : 10.1109/ARITH.2013.30
URL : https://hal.archives-ouvertes.fr/hal-00743090

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-point Algorithms in Coq [Coq12] The Coq development team. The Coq proof assistant reference manual , 2012. Version 8.4. [Fig95] Samuel A. Figueroa. When is Double Rounding Innocuous? SIGNUM Newsl IEEE Standard for Floating-Point Arithmetic, Proceedings of the 20th IEEE Symposium on Computer ArithmeticMDMM13] ´ Erik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double rounding, pp.243-25221, 1995.