Computability in Europe 2006
Logical Approaches to Computational Barriers


Regular Talk:
Coinductive Proofs for Basic Real Computation


Speaker: Tie Hou
Slot: Array, 11:10-11:30, col. 4

Abstract

We describe two representations for real numbers, signed
digit streams and Cauchy sequences. We give coinductive proofs for the
correctness of functions converting between these two representations to
show the adequacy of signed digit stream representation. We also show
a coinductive proof for the correctness of a corecursive program for the
average function with regard to the signed digit stream representation.
We implemented this proof in the interactive proof
system Minlog. Thus,
reliable, corecursive functions for real computation can be guaranteed,
which is very helpful in formal software development for real numbers.

websites: Arnold Beckmann 2006-04-22