The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Eric,

 

is it really so that floats don’t commute? I thought floats are commutative under addition and multiplication, but not associative. But maybe there are some exceptions I didn’t see as yet.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Eric Mullen
Sent: Sunday, July 05, 2015 1:12 AM
To: coq-club
Subject: Re: [Coq-Club] Machine floats in Coq

 

There's Flocq, which is used by CompCert to formalize floating point: http://flocq.gforge.inria.fr/

As for relating it to rationals, that will be tough. Rational arithmetic is quite fundamentally different than floating point: e.g. addition commutes in the rationals, but doesn't in the floats.

Best of luck!

Eric

 

On Sat, Jul 4, 2015 at 2:32 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Hi,

 

Some of my Coq programs need to interoperate (after extraction to Haskell)

with some Haskell libraries which use floating points (Prelude.Float).

 

Has someone axiomatized an interface to Haskell floats,

along with extraction-directives to realize those axiomatic operations with Haskell functions?

If so, I would be grateful to reuse that code and benefit from their experience.

 

It would be awesome if this interface also includes a logical specification of the floating point operations, perhaps in terms of Coq rationals (Coq.QArith.QArith_base.Q).

 

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

HTML Version:

---------------------------------------------------------------------
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies.