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.

Research

My main research interests are programming language design, automated reasoning for formal methods, and logic instrumented network dataflow analysis.

Manually specified verification offloads the challenge of deriving static guarantees to developers who lack the domain-specific expertise or time to become reasonable proof engineers. To address this issue, I am developing type systems that guarantee soundness without additional specifications. My goal is that all well-typed programs will 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.

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). I began exploring this idea in Sound Default-Typed Scheme.

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 my research? Please reach out!

Community

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