Russell O'Connor (RU Nijmegen): A Monadic Approach to
Certified Exact Real Arithmetic
Large scale real number computation is an essential
ingredient in several modern mathematical proofs. Because
such lengthy computations cannot be verified by hand,
one turns to software proof assistants to verify these
proofs. This talks presents a new implementation of the
constructive real numbers and elementary functions for
that uses the monad properties of the completion operation
on metric spaces. I believe that this approach yields
a real number library that is reasonably efficient for
computation, and yet simple enough to easily verify its
correctness.