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 interests involve developing practical frameworks for specifying program behaviors and using automated theorem provers to guarantee such specifications via behaviorally-sound type systems.

Research

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

Before that, I worked under Dr. Jonathan Aldrich at CMU thanks to the REUSE program. We developed a Gradual Verifier which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program. I’ve worked on the first ever gradual verification tool – Gradual C0 – and gradual verification in blockchain programming languages.

And even before that, I started doing Computer Science research under Dr. Adrian Sampson in the Calyx project. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.

Community

Outside of Cornell, I’m part 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 please check out the SIGPLAN YouTube Channel if you’re interested in some cool PL videos!