Re: [isabelle] Executing real numbers as approximating functions

On Wed, Aug 8, 2012 at 9:47 PM, Florian Haftmann
<florian.haftmann at> 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:

This page contains links to a couple of related papers.

- Brian

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