A computer verified, monadic, functional implementation of the integral

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.

References in corpus (3)

• A Monadic, Functional Implementation of Real Numbers
• Computing with Classical Real Numbers
• A Computer Verified Theory of Compact Sets

Cited by in corpus (5)

• Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
• Type classes for efficient exact real arithmetic in Coq
• Computer certified efficient exact reals in Coq
• Extracting efficient exact real number computation from proofs in constructive type theory
• Constructive Theory of Banach algebras