A coinductive approach to verified exact real number computation

Ulrich Berger, Sion Lloyd

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.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.23.331

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.23.331.307

Hosted By Universit├Ątsbibliothek TU Berlin.