Computer certified efficient exact reals in Coq

Articles

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

Slides

• TYPES. September 9, 2011, Bergen, Norway. [pdf]
• The Coq Workshop. August 26, 2011, Nijmegen, the Netherlands. [pdf]
• Conference on Intelligent Computer Mathematics. July 23, 2011, Bertinoro, Italy. [pdf]
• Brouwer seminar. March 22, 2011, Radboud University, Nijmegen, the Netherlands. [pdf]
• Workshop on reification and generic tactics. March 31, 2011, INRIA, Paris, France. [pdf]

Coq sources

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

https://github.com/robbertkrebbers