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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and