The Coq mailing list

[Noah Evans <noah.evans AT gmail.com>]

I second Richard's request.

On Sun, Jan 27, 2019 at 7:34 PM Richard Ford <richardlford AT gmail.com> wrote:

I'd like to see the sources for Chapter 9, the wave equation solution.

On Fri, Jan 25, 2019 at 6:49 AM Sylvie Boldo <sylvie.boldo AT inria.fr> wrote:

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