About

I’m an incoming CS PhD student in the POPV research group at Boston University co-advised by Ankush Das and Marco Gaboardi.

At one time, I did my undergraduate at Cornell University, where I studied computer science, mathematics, and analytical philosophy. I earned a degree in philosophy with a concentration in philosophy of mathematics, logic, and type theory.

I view my philosophical preparation in formal epistemology and logics as an essential framework to aid navigate my main technical interests: programming languages, automated reasoning, 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

I am uninspired by our current suite of languages that make use of manually specified formal specs. These tend to offload the intellectual challenge of coming up with exhaustive static guarantees to developers, those which don’t have the domain-specific expertise or simply time to become reasonable proof engineers.

I develop type systems to guarantee behavioral soundness while easing 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 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 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 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/Video 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.