Re: [isabelle] Executing real numbers as approximating functions



On Wed, Aug 8, 2012 at 9:47 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi all,
>
> 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

This page contains links to a couple of related papers.

- Brian





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