Computer certified efficient exact reals in Coq

Articles

• Robbert Krebbers and Bas Spitters, Type classes for efficient exact real arithmetic in Coq. Submitted. [pdf]
• Robbert Krebbers and Bas Spitters. Computer certified efficient exact reals in Coq. In CICM, volume 6824 of LNAI, pages 90-103, 2011. [pdf]

Slides

• Brouwer seminar. March 22, 2011. [pdf]
• Workshop on reification and generic tactics. March 31, 2011 at INRIA Paris. [pdf]

Coq sources

Our Coq and Haskell sources can be obtained from our GitHub repository.

https://github.com/robbertkrebbers