Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

Regular Talk:
Coinductive Proofs for Basic Real Computation

Speaker: Tie Hou
Presentation: Tie.pdf
Slot: Tue, 11:10-11:30, Faraday D (col. 4)


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 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by