A coinductive approach to verified exact real number computation

Authors

  • Ulrich Berger
  • Sion Lloyd

DOI:

https://doi.org/10.14279/tuj.eceasst.23.331

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.

Downloads

Published

2009-12-17

How to Cite

[1]
U. Berger and S. Lloyd, “A coinductive approach to verified exact real number computation”, eceasst, vol. 23, Dec. 2009.