Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq.

Sylvie Boldo Guillaume Melquiond

Published in: IEEE Symposium on Computer Arithmetic (2011)

Keyphrases

floating point
interval arithmetic

fixed point
sparse matrices

data structure
low cost

post processing
embedded systems