There is an implementation of exact real arithmetic that has been verified in in Coq[1] and also an implementation in Haskell[2] which may or may not do what you want to do.

It really does depend on what you want to compute. For instance, I can provide a simple implementation in Haskell that includes addition, multiplication and square roots: data Real = Real

  add :: Real -> Real -> Real
  add _ _ = Real 

  multiply :: Real -> Real -> Real
  multiply _ _ = Real

  squareRoot :: Real -> Real -> Real
  squareRoot _ _ = Real
 
  zero :: Real
  zero = Real

  one :: Real 
  one = Real

but it isn't very interesting as you can't print things or test for equality...Any implementation of real numbers that includes those is going to be much harder[3].

[1]http://videolectures.net/aug09_spitters_oconnor_cvia/ [2]http://www.haskell.org/haskellwiki/Exact_real_arithmetic [3]http://en.wikipedia.org/wiki/Tarskis_undefinability_theorem