About

I’m pursuing a PhD in programming languages at Boston University as part of the POPV research group, co-advised by Ankush Das and Marco Gaboardi. I did my undergrad at Cornell University, where I studied Computer Science and Philosophy.

You can find links to some of my hobbies in the navigation bar of this site. I enjoy digital photography, and am an aspiring amateur birder after being motivated by Cornell’s Ornithology Lab. I am also an avid enthusiast of 20th century history, with some favorite topics of interest being Irish revolutionary history, Polish shock therapy via the Balcerowicz Plan, and the fall of Francoist Spain.

Research

I am not convinced by the demanding workflow of current suite of languages that require manual work in a specification language on top of the implementation language. These offload the intellectual challenge of coming up with static guarantees to developers, many of whom either don’t have the domain-specific expertise or the time to become reasonable proof engineers. This has motivated my main interests: programming languages, formal methods for software engineering, and automated reasoning.

To address this issue, I develop type systems to guarantee behavioral soundness while easing/eliminating the need of directly specifying code behavior. I want to assure all well-typed and well-constructed programs imply well-behaved programs. I primarily make use of gradual, dependent/refinement, and probabilistic/plausibilistic types, in tandem with proof mining, automation, and repair.

I am currently working on:

Plausibilistic type systems: Qualitative notion of probabilistic type systems (such as PReST) using Halpern’s plausibility measures for a more generalized belief model enriched with default reasoning. Started playing around with this idea with Sound Default-Typed Scheme.

Gradual refinement types: Generalizing Igarashi’s notion of gradual session types to refinement types.

Automatic type-based verification: Automating refinement type systems with monadic effects with Hiroshi’s Constraint Horne Clauses solver.

I have previously worked on:

NetQIR: I interned at NASA Langley’s Formal Methods Research Program as part of the Safety-Critical Avionics Systems Branch under the advisory of Alwyn Goodloe. We mechanized proofs in Rocq that guarantee correct behaviors behind a well-behaved implementation of a Software Defined Delay-Tolerant Network algorithm written in P4 for NASA’s Interplanetary Overlay Network framework. These guarantees are then provided to the user at the type level when written in our DSL, NetQIR, which compiles a subset of P4 to our verified representation for machine checking.

Gradual Verification: I’m a 2× CMU REUSE alumni. I worked under the advisory of 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.

Calyx: I worked with the Computer Architecture & Programming Abstractions group at Cornell while advised by Adrian Sampson. I studied how to reason about modelling concurrency at the hardware-level for FPGA programming in Calyx using symbolic execution and KATs.

Interested in any of my ongoing research, past projects, or research philosophy? Feel free to reach out! I am also an active SIGPLAN community member, so you can probably catch me at any of the big-four SIGPLAN conferences.

Community

I’m a member of the Audio/Video team for SIGPLAN conferences. While this is just volunteering work, we’ve come to put a considerable amount of time and effort into making conferences run as smoothly as possible! 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.