The Coq mailing list

[Laurence Rideau <Laurence.Rideau AT inria.fr>]

Hello Richard,
you can get the Flocq sources here:

http://flocq.gforge.inria.fr/

Cheers

laurence



Le 24/01/2019 à 22:48, Richard Ford a écrit :
> 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?