Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.tcs.2005.09.061 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
exact computation,interactive theorem proving,Program and system verification,logical frameworks,corecursive proof,coinductive type theories,Lazy functional algorithms,program and system verification,corecursive implementation,Exact computation,corecursive algorithm,constructive real number,Coinductive type theories,coq.,streams of digits,Coq,coinductive type,logical framework Coq,real number,Streams of digits,exact real number,minimal axiomatization,Interactive theorem proving,lazy functional algorithms,infinite sequence,Logical Frameworks | Journal | 351 |
Issue | ISSN | Citations |
1 | Theoretical Computer Science | 18 |
PageRank | References | Authors |
1.01 | 10 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alberto Ciaffaglione | 1 | 58 | 9.97 |
| pietro di gianantonio | 2 | 167 | 17.30 |