The Coq mailing list

[Sylvie Boldo <sylvie.boldo AT inria.fr>]

Hello Richard,

Thanks for the praise!
The book is mostly based on Flocq, available (as said) on
http://flocq.gforge.inria.fr/ and also by opam : coq-flocq.

I am unsure about which other part you might be interested. In particular, the 
program proofs depend upon certain given versions of the tools so they are more 
difficult to communicate. Anyway, if you need some pointers, just tell me.

About the Runge-Kutta methods, this is precisely work-in-progress!
With Alexandre Chapoutot and Florian Faissole, we have developed pen-and-paper 
proofs of the rounding errors of Runge-Kutta schemes. See
https://hal.inria.fr/hal-01581794v1
https://hal.inria.fr/hal-01883843v1
A Coq formalization based on Flocq is in progress and will be probably be 
completed by the summer.

Hope this helps,

Sylvie


On 24/01/2019 22:48, Richard Ford wrote:
> One of my favorite books recently is "Computer Arithmetic and Formal Proofs" by 
> Sylvie Boldo and Guillaume Melquiond. It seems like a "must have" book for 
> anyone trying to prove things about  floating-point computations.
>
> I've studied it carefully but would like to take it to the next step by studying 
> the Coq sources, if they are available. I have already done some studying of the 
> sources of Flocq, either separately, or the version embedded within CompCert.
>
> Sylvie or Guillaume, are these sources available?
>
> Thanks for your work in producing this book!
>
> Richard L Ford
>
> P.S. I also appreciate the Coquelicot package. Is anyone aware of a 
> formalization of error bounds on the initial value problem for a system of first 
> order differential equations, e.g. solving using Euler or Runge-Kutta numerical 
> solutions?


--
Sylvie Boldo, projet Toccata, Inria Saclay - Île-de-France
PCRI, Bât. 650 - Université Paris-Sud - 91405 ORSAY Cedex