Exact computations with Newton's method

Ioana Pasca
Nicolas Julien

We consider Newton's method in the context of formally verified algorithms. We implement this method in a library of certified exact real arithmetic and prove the correctness of some algorithms based on Newton's method.

A paper describing this work has been submitted at TPHOLs [ pdf ].
We provide the following:

the proof of correctness for Newton's method implemented on axiomatic reals in Coq [ pdf ].
a full package of the Coq development including the exact reals library, the correctness for Newton's method and the certified algorithm [ source ]
More information about the exact reals library used can be found here