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/[EMAIL PROTECTED] _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
