49 citations · 191 across the 12 of their papers we have counts for
4 papers · 1 filter
Computing with Classical Real Numbers
Cezary Kaliszyk, Russell O'Connor
There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN lib…
A computer verified, monadic, functional implementation of the integral
Russell O'Connor, Bas Spitters
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 begi…
A Computer Verified Theory of Compact Sets
Russell O'Connor
Compact sets in constructive mathematics capture our intuition of what computable subsets of the plane (or any other complete metric space) ought to be. A good representation of co…
Certified Exact Transcendental Real Number Computation in Coq
Russell O'Connor
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implem…