We provide a computer verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by OConnor, this may be seen as the beginning of the realization of Bishops vision to use constructive mathematics as a programming language for exact analysis.
Download