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.
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:
PDFDOI: 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.