Research Software

CVC4
A constraint solver and automatic theorem prover for Satifiability Modulo Theories (SMT). I've worked on proofs for bit-vectors and arithmetic. [site] [code]
LFSC
A dependently typed language for expressing SMT proofs. I've touched most parts of it. [code]
Bellman Bignat
A SNARK-friendly implementation of multiprecision arithmetic, hash-to-prime, Wesolowski proofs of exponentiation, and RSA accumulators using the Bellman library. [code]

Independent Work

Construct
A programming language and interactive tool for classical geometry. [site] [code]
Khwarizmi
A programming language for algebra. A work in progress. [site] [code]
notebk
The program I use for managing my electronic notebook. It has exactly the interface I want. [code]

Internships

Coursera
2018
Improving developer infrastructure and doing the early design for various projects. [post]
Coursera
2017
Enabling collaboration within the course platform.
Facebook
2015
Prototyping a data movement system. It has since been productionized.
JP Morgan
2014
Building settlement software and reverse-engineering closed-source toolkits. Learning to program.