A coinductive approach to verified exact real number computation

Abstract

We present an approach to verified programs for
exact real number computation that is based on inductive and
coinductive definitions and program extraction from proofs.
We informally discuss the theoretical background of this method
and give examples of extracted programs implementing
the translation between the representation by fast converging
rational Cauchy sequences and the signed binary
digit representations of real numbers.