coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Richard Ford, 01/24/2019
- Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Laurence Rideau, 01/25/2019
- Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Sylvie Boldo, 01/25/2019
- Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Richard Ford, 01/28/2019
- Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Noah Evans, 01/29/2019
- Re: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?, Richard Ford, 01/28/2019
Archive powered by MHonArc 2.6.18.