TL;DR
This paper presents a formally verified, monadic, functional implementation of the Riemann integral within type theory, advancing the use of constructive mathematics for exact analysis in programming.
Contribution
It introduces a computer verified, exact monadic functional implementation of the Riemann integral, supporting Bishop's vision of constructive mathematics as a programming language.
Findings
Verified correctness of the integral implementation
Supports exact analysis in constructive mathematics
Builds on previous work to advance formal methods
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
