Milad Niqui. Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers. In Thorsten Altenkirch, Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Volume 4502 of Lecture Notes in Computer Science, pages 203-220, Springer, 2006. [doi]