Berger, Ulrich, and Sion Lloyd. “A Coinductive Approach to Verified Exact Real Number Computation”. Electronic Communications of the EASST, vol. 23, Dec. 2009, doi:10.14279/tuj.eceasst.23.331.