A Survey of Exact Arithmetic Implementations. - Paul Gowland; David R. Lester (CCA, 2000)

Using PVS to validate the algorithms of an exact arithmetic. - David R. Lester; Paul Gowland (Theor. Comput. Sci., 2003)