Coinductive Formal Reasoning in Exact Real Arithmetic

In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by coinductive streams. The algorithms work on coinductive stream of M

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Milad Niqui
• Keywords: Algorithms, Coinductive Stream, CORR 2008, Education, Real Numbers