2015/11/03 by Ulrich Berger, Berger, Ulrich, Sion Lloyd +1
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Numerical Methods and Algorithms
paper · doi:10.14279/tuj.eceasst.23.331
openalex publication_date 2024/03/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
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.