coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] float numbers

From: Kate Fairchild <Kate.Fairchild AT addisongroup.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] float numbers
Date: Wed, 16 Aug 2017 13:43:07 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Kate.Fairchild AT addisongroup.com; spf=Pass smtp.mailfrom=Kate.Fairchild AT addisongroup.com; spf=None smtp.helo=postmaster AT mail.addisongroup.com
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024;d=addisongroup.com; h=from:to:subject:date:message-id:references:in-reply-to:content-type :mime-version; b=GCS5aKy1SFSOm1hMaCkXgvlztFT/aIyUipmXMpNDc7SVZ0R2ppW20pkL3UFTgKh3aAMM10Bk QW7xNN9rOnLlCLWia/JusBdDFDdCsrH19zfT6mXLQ6TKISQmSa7WB2S1c7fCBrV4kZeg867G FXdMIXlkp3Vm6ccayWS+r1rF/FE=
Ironport-phdr: 9a23:e4Et4RFBexHuH9VJTZTBiJ1GYnF86YWxBRYc798ds5kLTJ75psSwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQMUAQj1YBVqOaL8FoLTlMOx2Pq15oWVaAJN1wa6NPl5KwzzpgHMvOEXh5FjI+A/0FGB9nBPYqFdwX5iDVOVhRf1oMmqqs1N6SNV7tEo68MIf6z7Za84TLhURGAFOnw4ouPitAPITQqL6lMVXmkXiR1ODBLC8Qm8VZD05Hip/tFh0TWXaJWlBYs/Xi6vuv9m

Can I please be removed from this list?

Kate Fairchild
Recruiting Manager - Information Technology
Addison Group
kate.fairchild AT addisongroup.com

14160 Dallas Parkway Suite 400
Dallas, TX 75254

-----Original Message-----
From:
coq-club-request AT inria.fr

[mailto:coq-club-request AT inria.fr]
On Behalf Of Guillaume Melquiond
Sent: Wednesday, August 16, 2017 8:34 AM
To:
coq-club AT inria.fr
Subject: Re: [Coq-Club] float numbers

On 15/08/2017 08:05, karsar wrote:
> What would be a natural choice of float number library if you want to
> do some computations with floats inside Coq (like it's done for
> integers and nats, I know it could be slow) , as well as reason about
> their properties?
> It would be nice to provide a minimal example script showing how you
> import the library and example of the addition of two floats as a
> demonstration.

Both the Flocq and Interval libraries contain computationally effective
floating-point components. Which one to use and how to use it depend on your
use case. Do you need the floating-point numbers to be compliant with the
IEEE-754 standard? What kind of reasoning do you want to perform on them? How
efficient do you want the computations to be?

Best regards,

Guillaume

This message contains confidential information and is intended only for the
individual named. If you are not the named addressee you should not
disseminate, distribute or copy this e-mail. Please notify the sender
immediately by e-mail if you have received this e-mail by mistake and delete
this e-mail from your system. E-mail transmission cannot be guaranteed to be
secure or error-free as information could be intercepted, corrupted, lost,
destroyed, arrive late or incomplete, or contain viruses. The sender
therefore does not accept liability for any errors or omissions in the
contents of this message, which arise as a result of e-mail transmission.
Should you wish to be excluded from any future mailings, please send an email
to
unsubscribe AT addisongroup.com
with the word unsubscribe in the subject. If verification is required
please request a hard-copy version. Addison Group, 125 S Wacker Dr, 27th
Floor, Chicago, IL, www.addisongroup.com

[Coq-Club] float numbers, karsar, 08/15/2017
- Re: [Coq-Club] float numbers, Laurent Thery, 08/15/2017
- Re: [Coq-Club] float numbers, Guillaume Melquiond, 08/16/2017
  - RE: [Coq-Club] float numbers, Kate Fairchild, 08/16/2017
    - Re: [Coq-Club] float numbers, karsar, 08/20/2017