Affine functions and series with co-inductive real numbers

Yves Bertot

We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits impleme…