El creador de ese hilo comunicó que usó Decimal64. No es una librería, pero a lo mejor para lo que lo necesitas te sirve. Sinceramente, no lo he usado así que no te puedo detallar nada salvo esto:

http://en.wikipedia.org/wiki/Decimal64_floating-point_format