Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?


Chronological Thread 
  • From: Laurence Rideau <Laurence.Rideau AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?
  • Date: Fri, 25 Jan 2019 08:53:18 +0100

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?





Archive powered by MHonArc 2.6.18.

Top of Page