completion monad

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

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.

The completion monad was introduced in

- Russel O'Connor,
*A Monadic, Functional Implementation of Real Numbers*MSCS, 17(1):129-159, 2007 (arXiv:cs/0605058)

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

- Robbert Krebbers, Bas Spitters,
*Type classes for efficient exact real arithmetic in Coq*(arXiv:1106.3448)

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