Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (2012)