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

[Bill Page]

Changes http://page.axiom-developer.org/zope/mathaction/RealNumbers/diff
--
A certified, corecursive implementation
of exact Real Numbers

Alberto Ciaffaglione a, Pietro Di Gianantonio

http://www.dimi.uniud.it/~ciaffagl/Papers/reals.pdf

Abstract
We implement exact real numbers in the logical framework Coq using streams, 
i.e.,
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 http://page.axiom-developer.org/zope/mathaction/address@hidden