A coinductive approach to verified exact real number computation - Berger, Ulrich; Lloyd, Sion (Electronic Communications of the EASST, 2009)
We present an approach to verified programs for exact real number computation that is based on inductive andcoinductive definitions and program extraction from proofs.We informally discuss the theoretical background of this methodand give examples of extracted programs implementing the translation between the representation by fast convergingrational Cauchy sequences and the signed binarydigit representations of real numbers.