The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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/