Russell O'Connor

29 papers B 1C 1Journal 20Unranked 7
YearRankTypeTitle / Venue / Authors
2025 J jnl
Formal Verification of the Safegcd Implementation.
CoRR
Russell O'Connor, Andrew Poelstra
2018 J jnl
Theory Presentation Combinators.
CoRR
Jacques Carette, Russell O'Connor
2017 — conf
Enhancing Bitcoin Transactions with Covenants.
Financial Cryptography Workshops
Russell O'Connor, Marta Piekarska
2017 — conf
Simplicity: A New Language for Blockchains.
PLAS@CCS
Russell O'Connor
2017 J jnl
Simplicity: A New Language for Blockchains.
CoRR
Russell O'Connor
2015 J jnl
A representation theorem for second-order functionals.
J. Funct. Program.
Mauro Jaskelioff, Russell O'Connor
2014 J jnl
A Representation Theorem for Second-Order Functionals.
CoRR
Mauro Jaskelioff, Russell O'Connor
2013 B conf
A Machine-Checked Proof of the Odd Order Theorem.
ITP
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
2012 J jnl
Theory Presentation Combinators
CoRR
Jacques Carette, Russell O'Connor
2012 — conf
Theory Presentation Combinators.
AISC/MKM/Calculemus
Jacques Carette, Russell O'Connor
2011 J jnl
Classical mathematics for a constructive world.
Math. Struct. Comput. Sci.
Russell O'Connor
2011 J jnl
Functor is to Lens as Applicative is to Biplate: Introducing Multiplate
CoRR
Russell O'Connor
2011 — conf
MathScheme: Project Description.
Calculemus/MKM
Jacques Carette, William M. Farmer, Russell O'Connor
2011 J jnl
The MathScheme Library: Some Preliminary Experiments
CoRR
Jacques Carette, William M. Farmer, Filip Jeremic, Vincent Maccio, Russell O'Connor, Quang M. Tran
2011 — conf
Video presentation of Functor : Lens : : Applicative : Biplate: Introducing Multiplate.
WGP@ICFP
Russell O'Connor
2010 J jnl
A computer-verified monadic functional implementation of the integral.
Theor. Comput. Sci.
Russell O'Connor, Bas Spitters
2010 J jnl
Classical Mathematics for a Constructive World
CoRR
Russell O'Connor
2010 J jnl
L-plotting - A method for visual analysis of physiological experimental and modeling multi-component data.
Neurocomputing
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
2009 C conf
Computer Verified Exact Analysis (Tutorial).
CCA
Bas Spitters, Russell O'Connor
2009 J jnl
Computing with Classical Real Numbers.
J. Formaliz. Reason.
Cezary Kaliszyk, Russell O'Connor
2008 J jnl
A Computer Verified Theory of Compact Sets
CoRR
Russell O'Connor
2008 J jnl
A computer verified, monadic, functional implementation of the integral
CoRR
Russell O'Connor, Bas Spitters
2008 J jnl
Certified Exact Transcendental Real Number Computation in Coq
CoRR
Russell O'Connor
2008 — conf
Certified Exact Transcendental Real Number Computation in Coq.
TPHOLs
Russell O'Connor
2008 J jnl
Computing with Classical Real Numbers
CoRR
Cezary Kaliszyk, Russell O'Connor
2007 J jnl
A monadic, functional implementation of real numbers.
Math. Struct. Comput. Sci.
Russell O'Connor
2006 J jnl
A Monadic, Functional Implementation of Real Numbers
CoRR
Russell O'Connor
2005 J jnl
Essential Incompleteness of Arithmetic Verified by Coq
CoRR
Russell O'Connor
2005 — conf
Essential Incompleteness of Arithmetic Verified by Coq.
TPHOLs
Russell O'Connor