coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Richard Ford <richardlford AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq sources for "Computer Arithmetic and Formal Proofs"?
Date: Thu, 24 Jan 2019 15:48:01 -0600
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richardlford AT gmail.com; spf=Pass smtp.mailfrom=richardlford AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f182.google.com
Ironport-phdr: 9a23:jXYKVBTUKkjwEkCtGzL7aapFn9psv+yvbD5Q0YIujvd0So/mwa69ZBGN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27XhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBE+sBMvpYr4bnvVsBsAa1CwmrBOP11zBDm3j73bc70+s9EQHJxhYgEM8KsHTaq9X1LrodXPu6zKnN1zrDbvdW1S3h54jPdxAsuPeBVq9zf8rJ0UQjCR/Jg1GKpYHmPz6ZzPoBv3Wf4uZ6SO6iiHArpgdsqTa13MgskJPGhocNx1DE6yp5xIE1KMW9SEFhYN6kFIJctiGBOIdrW88iTXxktSUkxrEctp67ey8KyJsjxxHBcfCIb4+I4hf7WOaQJzd3mm5ldaqhixqu9UWs0O7xW8mu3FpUsyZIlsPAum0O2hDN8sSHT+Fy/kal2TaBzQDT7eRELFgularaN5EhwqQ/loAOvkTHEC/2n1/2g7KNe0Ur/+in8eXnYrH8qpCAMI90jxnyMr4ylcynHeQ4Lg8OUnCH9uS7zb3v5FH2QLFXjvItiaTZq5DbJcEDpqGjGQNV04Aj6wy+Dzi8ytgYk2MHfxp5f0eMiJGsMFXTKtj5C+2+ihKiimRF3ffDa4fgCZXENHSLvrD7cf4p8U9XyAMpwdRR4IhYIr4EKfP3HET2sYqLXVcCLwWozrO/W51G3YQEVDfXW/7LAObpqVaNo9kXDayJbY4Rtiz6LqF8tfHrhH4931QaePvwhMdFWDWDBv1jZn6hTz/0mN5YSDUFuwM/SKrhj1jQCWcONUb3ZLo143QAMKzjDYrHQdrz0rmI3SP+D5cPI24fWgrKHnDveIGJHfwLbXDKLw==

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