Software

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.