[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] [RealNumbers] implementing Exact Real Numbers

From: Bill Page
Subject: [Axiom-developer] [RealNumbers] implementing Exact Real Numbers
Date: Wed, 15 Jun 2005 04:08:06 -0500

A certified, corecursive implementation
of exact Real Numbers

Alberto Ciaffaglione a, Pietro Di Gianantonio

We implement exact real numbers in the logical framework Coq using streams, 
infinite sequences, of digits, and characterize constructive real
numbers through a minimal axiomatization. We prove that our
construction inhabits the axiomatization, working formally with
coinductive types and corecursive proofs. Thus we obtain reliable,
corecursive algorithms for computing on real numbers.

forwarded from

reply via email to

[Prev in Thread] Current Thread [Next in Thread]