About

I’m an incoming CS PhD student! At one time, I did my undergraduate at Cornell University, where I studied Computer Science, Mathematics, and earned a degree in Philosophy with a concentration in Philosophy of Mathematics and Logic supervised by Dr. Harold T. Hodes.

I view my philosophical preparation in formal epistemology and logics as an essential framework to aid navigate my main technical interests: program synthesis and repair, programming languages theory, and formal methods for software engineering.

Personally, I’m an avid cinephile and audiophile, for which you can find a rabbit-hole of information at the top right of this page. I also enjoy digital photography, and am amateurly practicing birding after getting inspired by Cornell’s Ornithology Lab. Some day, I want to learn to shoot/develop film, get a US Amateur Radio License, and successfully pick an Abloy Protec2.

Research

Most formal verification toolchains feel uninspiring to me because they make it challenging to prioritize static guarantees given their technical complexity, especially given that lightweight methods provide reasonable results in their stead (at the cost of runtime overhead). My current research involves developing practical frameworks for specification-driven program verification to ease the need/complexity of directly mechanizing code. I want to assure all well-typed and well-constructed programs imply well-behaved programs.

Previously, during my undergrad, I worked on—broadly—three projects:

• RocqNet : Advised by Dr. Alwyn Goodloe at NASA’s Langley Formal Methods, we mechanized 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.

• Calyx : Advised by Dr. Adrian Sampson at the Computer Architecture & Programming Abstractions group. Here, I studied how to reason about modelling hardware-level parallelism for Calyx using symbolic execution and KATs.

• Gradual Verification : 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.