The Coq mailing list

[Eric Mullen <emullen AT cs.washington.edu>]

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/