I'm a former academic looking to transition to a full-time role in industry. Some projects that I'm currently or have recently worked on:

• A bytecode compiler for Lisp written in C++
• sarah-connor: A termination checker for LLVM IR programs
• single-file-devin: An LLM-powered software engineering agent for single-file Python programs.

I've also worked on a few different research projects in the areas of Programming Languages, Compilers, and Formal Methods during my time in college and grad school:

• I wrote a Continuation-Passing Style transformation for the CertiCoq compiler and helped proved its semantic correctness.
• I developed and implemented an algorithm for synthesizing (automatically generating) string-manipulating programs modeled as transducers from formal specifications using an SMT solver. This project was published as a paper.
• Most recently, I was working on a technique for synthesizing formal semantics of languages using language interpreters as oracles. I have also worked on projects in automated program verification and have experience applying formal methods in industry.

A few miscellaneous programming projects:

• models-from-scratch: Implementations of logistic regression, decision trees, and k-nearest neighbors in Python.
• tcp-flow-control: An implementation of the flow control algorithm used for TCP using the socket library in Python.
• recursion-schemes-synthesis: A toy project exploring program synthesis using catamorphisms.

You can find more biographical and work related details on my LinkedIn or personal website.