# Re: [isabelle] Executing real numbers as approximating functions

Hi Florian and Brian,
>> once I have heard about a formalisation to execute real numbers as
>> approximating functions, i.e. where each real number r is implemented
>> using a function
>>
>> R :: nat => float
>>
>> such that R n equals r approximated to the n-th digit (or something
>> similar).
>>
>> Can somebody give me a reference for that?
>
>Russell O'Connor has implemented a similar representation of the
>computable reals in Coq:
>
>http://corn.cs.ru.nl/library/fastreal.html
Bas Spitters points out to me that only in the work that
he and Robbert Krebbers did (which was a continuation of
Russell's work) floats were used in the representations.
Russell used rational numbers, I think.
I think that this move to floats (and other things that
they did, I'm sure) made the computations much faster.
See:
http://arxiv.org/abs/1106.3448/
http://robbertkrebbers.nl/research/reals/
Freek

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*