About

I’m a first-year PhD student in programming languages at Boston University, co-advised by Ankush Das and Marco Gaboardi. I’m affiliated with the POPV research group and with Logic @ BU, an interdisciplinary group spanning computer science, math, linguistics, and philosophy. I earned my BA from Cornell University, with a focus in 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 also have a strong interest in 20th-century history, with a particular focus on Irish revolutionary history, Poland’s economic transition via the Balcerowicz Plan, and the fall of Francoist Spain.

Research

I find myself not convinced by the demanding instrumentation required in static analysis. That is, manually specifying verification constraints in a specification language on top of the program logic in an 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 to become reasonable proof engineers or simply lack the time. This challenge motivates my main research interests: programming language design, automated reasoning for formal methods, and logic instrumented network dataflow analysis.

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 programs imply well-behaved programs.

Currently working on:

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

Continuous-time probabilistic types: Instrumenting probabilistic refinement session programs with a typed temporal analysis for guaranteeing timing constraints in distributed algorithms.

Typed automated verification: Automating verification of refinement type systems with monadic effects based on Hiroshi’s constraint horne clauses solver.

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.

“Disorganized” projects:

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

Interested in any of my ongoing research, past projects, or research philosophy? Feel free to reach out! I’m 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.