Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

14

CIE
2006
Springer

favoriteEmaildiscussreport

116views Applied Computing» more CIE 2006»

Coinductive Proofs for Basic Real Computation

13 years 8 months ago

Coinductive Proofs for Basic Real Computation

Download staff.science.uva.nl

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.

Tie Hou

Real-time Traffic

Applied Computing | CIE 2006 | Coinductive Proof | Digit Stream | Digit Stream Representation |

claim paper

Related Content

» Coinduction for Exact Real Number Computation

» Proofs Programs Processes

» Certified Exact Real Arithmetic Using Coinduction in Arbitrary Integer Base

» Feasible Functions over Coinductive Data

» Intrinsic Statistics on Riemannian Manifolds Basic Tools for Geometric Measurements

» The Methods of Approximation and Lifting in Real Computation

» The elementary computable functions over the real numbers applying two new techniques

» Random Oracle Instantiation in Distributed Protocols Using Trusted Platform Modules

» Performance Analysis of a Parallel Application in the GRID

Post Info
More Details (n/a)

Added	20 Aug 2010
Updated	20 Aug 2010
Type	Conference
Year	2006
Where	CIE
Authors	Tie Hou

Comments (0)