49 citations · 191 across the 12 of their papers we have counts for
7 papers · 1 filter
Building on the Diamonds between Theories: Theory Presentation Combinators
Jacques Carette, Russell O'Connor, Yasmine Sharoda
To build a large library of mathematics, it seems more efficient to take advantage of the inherent structure of mathematical theories. Various theory presentation combinators have…
Classical Mathematics for a Constructive World
Russell O'Connor
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively b…
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…