Meanwhile here is another - thank you to Freddie Witherden for both of these finds: "The Metalibm project provides a tool for the automatic implementation of mathematical (libm) functions. A function f is automatically transformed into Gappa-certified C code implementing an approximation polynomial in a given domain with given accuracy." Code: http://lipforge.ens-lyon.fr/www/metalibm/ Slides: http://tamadiwiki.ens-lyon.fr/tamadiwiki/images/d/d8/DeDinechin2013.pdf The context of this was the "STOKE" PLDI paper I mentioned last week, http://web.stanford.edu/~sharmar/pubs/fp.pdf The point being that MetaLibc produces approximated functions with proven properties, while STOKE stochastically searches for implementations that are "close enough" under testing. Paul Begin forwarded message: From: "Witherden, Freddie" <freddie.witherden08@imperial.ac.uk<mailto:freddie.witherden08@imperial.ac.uk>> Date: 21 June 2014 12:43:12 GMT+01:00 To: "Kelly, Paul H J" <p.kelly@imperial.ac.uk<mailto:p.kelly@imperial.ac.uk>> Subject: Math Libraries Hi Paul, With regards to our discussion last week on math libraries (and how you can apparently get away with flipping an instruction here and there) I am wondering if you have heard about metalibm: http://lipforge.ens-lyon.fr/www/metalibm/ http://tamadiwiki.ens-lyon.fr/tamadiwiki/images/d/d8/DeDinechin2013.pdf It is from the same group that developed crlibm. Regards, Freddie.