Publications
Refereed and Pending Publications
- Mauro Jaskelioff, Russell O’Connor. A Representation Theorem for Second-Order Functionals. Under consideration for the Journal of Functional Programming.
- Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry: A Machine-Checked Proof of the Odd Order Theorem. ITP 2013: 163-179
- Jacques Carette, Russell O’Connor. Theory Presentation Combinators. AISC/MKM/Calculemus 2012:202-215.
- Russell O’Connor. Functor is to Lens as Applicative is to Biplate: Introducing Multiplate. ACM SIGPLAN 7th Workshop on Generic Programming, Tokyo, Japan, 18th September 2011, arXiv:1103.2841v2 [cs.PL]
- Russell O’Connor. Classical Mathematics for a Constructive World. Mathematical Structures in Computer Science (2011), 21: 861–882
- Russell O’Connor and Bas Spitters. A Computer Verified, Monadic, Functional Implementation of the Integral. Theoretical Computer Science, Vol. 411, No. 37, Aug 2010, Pages 3386–3402
- Cezary Kaliszyk and Russell O’Connor. Computing with Classical Real Numbers. Journal of Formalized Reasoning, Vol. 2, No. 1, 2009, Pages 27–29
- Russell O’Connor. Certified Exact Transcendental Real Number Computation in Coq. TPHOLS 2008, LNCS 5170: 246–261, Aug 2008, Proceedings
- Russell O’Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08–08: 148–162, Jul 2008, Proceedings
- Russell O’Connor. A monadic, functional implementation of real numbers. Mathematical Structures in Computer Science, Feb 2007. Volume 17, Issue 1, pp. 129–159
- Russell O’Connor. Essential Incompleteness of Arithmetic Verified by Coq. Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLS 2005, Lecture Notes in Computer Science, Volume 3603, Aug 2005. Proceedings, pp. 245–260
Other Publications