Article ID Journal Published Year Pages File Type
438773 Theoretical Computer Science 2006 13 Pages 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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics