A computer verified, monadic, functional implementation of the integral

Joint work with Russel O'Connor

Bas Spitters

We provide a computer verified exact monadic functional implementation of the Riemann integral in constructive type theory. This may be seen as the beginning of the realization of Bishop's vision to use constructive mathematics as a high level programming language for exact analysis.

back to EIDMA Seminar Combinatorial Theory announcements