About

I’m a Senior (applying to Doctoral Programs!) at Cornell University working towards degrees in Computer Science with a concentration in Programming Languages & Philosophy with a concentration in Logic advised by Dr. Harold T. Hodes.

My main research interest involves developing practical frameworks for program verification by creating a set of canonical and reusable representations for domain-specific programs to ease the need to directly mechanize code with automated theorem provers. You can find my research statement here!

Research

I’m currenty working with Dr. Alwyn Goodloe at NASA’s Langley Formal Methods. We’re mechanizing proofs with Coq that model correct behaviors behind a well-behaved implementation of a Software Defined Delay-Tolerant Network’s Match-Action pipeline algorithm for NASA’s Interplanetary Overlay Network framework. The well-behavedness of the algorithm comes from it being implemented in our networks DSL: NetQIR !

I’m also working with Dr. Adrian Sampson on the Calyx project. Here, I’m figuring out how to model hardware-level parallelism using Kleene Algebra with Tests.

In addition, I’m a 2× CMU REUSE alumni. I worked under Dr. Jonathan Aldrich in developing a Gradual Verifier, seeking to bridge the gap between static and dynamic verification. I worked on the first ever gradual verification tool – Gradual C0 – and made use of gradual verification for blockchain programming languages.

Community

I’m a member of the Audio/Visual team for SIGPLAN conferences. While this is just volunteering work, I’ve come to put a considerable amount of time into it, so feel free check out SIGPLAN’s official YouTube Channel if you’re interested in some cool PL videos!

Tired of my site? Click here for a random one of my friends.