Formalization of Mathematics
In order to formally prove the corresponding programs, we need (applied) mathematics to be formalized too. Therefore, I have been involved in several libraries of formalized mathematics.
The coq-num-analysis library (also an opam package) includes many results of numerical analysis, including the Lebesgue integration of nonnegative functions and the Lax-Milgram theorem.
With François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis, we formally proved correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors.