Mathematics and Computation

A blog about mathematics for computers

Tutorial on exact real numbers in Coq

Already a while ago published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O'Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also gave a quick tutorial on Coq.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention, I will gladly respond. You are also welcome to contact me directly.