The Coq mailing list

[Milad Niqui <milad AT cs.ru.nl>]

Roland Zumkeller 
<Roland.Zumkeller AT polytechnique.fr>
 writes:

> I'm looking for a developement of exact real arithmetic in coq (if not
> available, in ml). Such a library should be able to calculate any 
> expression up
> to a given precision.
> This kind of real numbers are most commonly represented by infinite digit
> sequences or continuos fractions.
> Thank you for providing any references.
>


Dear Roland,

 You can have a look at my thesis which I defended recently (well,
 yesterday!). The title of the thesis is "Formalising exact Arithmetic"
 and deals with exact rational and real arithmetic in constructive type
 theory. Parts of the thesis are formalised in Coq. The thesis can be
 downloaded at the following URL:

  http://www.cs.ru.nl/~milad/proefschrift/thesis.pdf

Regards,

-- 
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
Radboud University Nijmegen,                 fax:+31 24 365 2728
P.O.B. 9010, 6500 GL Nijmegen,               email: milad <AT> cs.ru.nl
The Netherlands.                             http://www.cs.ru.nl/~milad