The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

I know of this, but haven't looked at it myself:
http://www.ps.uni-saarland.de/~hornung/bachelor.php

Kind regards, Jonas

2012/6/23 Vladimir Voevodsky 
<vladimir AT ias.edu>:
> I wonder if someone tried to build a constructive model of real numbers 
> starting with the floating point representations of increasing precision?
>
> Vladimir.
>
>