The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

We did something in that direction. The approximate rationals in math-classes.
https://github.com/math-classes

http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

It the time we could not directly connect it to flocq, but I
understand that should now be more stable.

Best,

Bas

On Sat, Jul 4, 2015 at 11:31 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/