A computer verified, monadic, functional implementation of the integral