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