Essential Incompleteness of Arithmetic Verified by Coq. - Russell O'Connor (TPHOLs, 2005)

A monadic, functional implementation of real numbers. - Russell O'Connor (Math. Struct. Comput. Sci., 2007)

Certified Exact Transcendental Real Number Computation in Coq. - Russell O'Connor (TPHOLs, 2008)

A Computer Verified Theory of Compact Sets - Russell O'Connor (CoRR, 2008)

Computer Verified Exact Analysis (Tutorial). - Bas Spitters; Russell O'Connor (CCA, 2009)

Computing with Classical Real Numbers. - Cezary Kaliszyk; Russell O'Connor (J. Formaliz. Reason., 2009)

L-plotting - A method for visual analysis of physiological experimental and modeling multi-component data. - Witali L. Dunin-Barkowski; Andrew T. Lovering; John M. Orem; David M. Baekey; Thomas E. Dick; Ilya A. Rybak; Kendall Francis Morris; Russell O'Connor; Sarah C. Nuding; Roger Shannon; Bruce G. Lindsey (Neurocomputing, 2010)

A computer-verified monadic functional implementation of the integral. - Russell O'Connor; Bas Spitters (Theor. Comput. Sci., 2010)

Video presentation of Functor : Lens : : Applicative : Biplate: Introducing Multiplate. - Russell O'Connor (WGP@ICFP, 2011)

MathScheme: Project Description. - Jacques Carette; William M. Farmer; Russell O'Connor (Calculemus/MKM, 2011)

Functor is to Lens as Applicative is to Biplate: Introducing Multiplate - Russell O'Connor (CoRR, 2011)

The MathScheme Library: Some Preliminary Experiments - Jacques Carette; William M. Farmer; Filip Jeremic; Vincent Maccio; Russell O'Connor; Quang M. Tran (CoRR, 2011)

Classical mathematics for a constructive world. - Russell O'Connor (Math. Struct. Comput. Sci., 2011)

Theory Presentation Combinators. - Jacques Carette; Russell O'Connor (AISC/MKM/Calculemus, 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

A representation theorem for second-order functionals. - Mauro Jaskelioff; Russell O'Connor (J. Funct. Program., 2015)

Simplicity: A New Language for Blockchains. - Russell O'Connor (PLAS@CCS, 2017)

Enhancing Bitcoin Transactions with Covenants. - Russell O'Connor; Marta Piekarska (Financial Cryptography Workshops, 2017)

Formal Verification of the Safegcd Implementation. - Russell O'Connor; Andrew Poelstra (CoRR, 2025)