A computer verified, monadic, functional implementation of the integral
Logic in Computer Science
2010-08-11 v2 Numerical Analysis
Abstract
We provide a computer verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by O'Connor, this may be seen as the beginning of the realization of Bishop's vision to use constructive mathematics as a programming language for exact analysis.
Cite
@article{arxiv.0809.1552,
title = {A computer verified, monadic, functional implementation of the integral},
author = {Russell O'Connor and Bas Spitters},
journal= {arXiv preprint arXiv:0809.1552},
year = {2010}
}