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

Sylvie Boldo, Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. In Elisardo Antelo, David Hough, Paolo Ienne, editors, 20th IEEE Symposium on Computer Arithmetic, ARITH 2011, Tübingen, Germany, 25-27 July 2011. pages 243-252, IEEE Computer Society, 2011. [doi]

Abstract

Abstract is missing.