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.
Previously, the CoRN project @cite_21 showed that the formalization of constructive analysis in a type theory is feasible. However, the extraction of programs from such developments is difficult @cite_19 . On the contrary, in the present article we have shown that if one takes an algorithmic attitude from the start it is possible to obtain feasible programs.
@cite_19 @cite_21
2096282101 1498091397
It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement these algorithms on a computer; moreover, one runs the risk of making mistakes in the process. We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a mathematical library of constructive algebra and analysis formalized in the theorem prover Coq. We explain the structure and the contents of the library and we discuss the motivation and some (possible) applications of such a library.