# Tutorial on exact real numbers in Coq

- 07 January 2010
- Computation, Constructive math, Programming, Tutorial

Already a while ago videolectures.net 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.

##### Post a comment:

Write your comment using Markdown.
Use

`$⋯$`

for inline and `$$⋯$$`

for display LaTeX formulas,
and `<pre>⋯</pre>`

for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.