Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
438773 | Theoretical Computer Science | 2006 | 13 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics