Contents

# Contents

## Idea

The completion monad is a monad (in computer science) which is used for exact computations with real numbers, in the sense of constructive analysis. It has been used for certified programming with guaranteed exactness of real number approximations.

## References

The completion monad was introduced in

and implemented in Coq in

• Russel O'Connor, Certified Exact Transcendental Real Number Computation in Coq In TPHOLs 2008, volume 5170 of LNCS, pages 246261, 2008.

For more see

Created on February 11, 2014 at 13:32:49. See the history of this page for a list of all contributions to it.