49 citations · 191 across the 12 of their papers we have counts for
14 papers
Formal Verification of the Safegcd Implementation
Russell O'Connor, Andrew Poelstra
The modular inverse is an essential piece of computation required for elliptic curve operations used for digital signatures in Bitcoin and other applications. A novel approach to t…
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…
Simplicity: A New Language for Blockchains
Russell O'Connor
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve…
A Representation Theorem for Second-Order Functionals
Mauro Jaskelioff, Russell O'Connor
Representation theorems relate seemingly complex objects to concrete, more tractable ones. In this paper, we take advantage of the abstraction power of category theory and provide…
Theory Presentation Combinators
Jacques Carette, Russell O'Connor
We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category o…
The MathScheme Library: Some Preliminary Experiments
Jacques Carette, William M. Farmer, Filip Jeremic +3
We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for o…