My Projects

Advisor: Ethan Cecchetti

Choreographic programming is an approach to distributed systems programming that guarantees deadlock-freedom by programming from a global perspective rather than programming each participant separately. Under Ashley's guidance, I contributed to her research on extending Choreographic Programming with features as first class locations, process forking, etc.
My contribution focuses on algorithmic typing. I formalized an example local language with a type-and-effect system, and parameterized the Choreography over its abstract interface. I designed bidirectional checking/inference algorithms at both levels and proved its soundness and completeness in Rocq. The formalization includes subtyping, effect judgments, and multiple levels of sorts. In particular, my work is the first to establish typing decidiblity of this class of System-F like Choregraphic Languages.

Advisor: Ethan Cecchetti

Effect systems statically approximate the computational behavior of programs, but designing inference algorithms for each new effect systems can be brittle and time consuming. I investigated the possibility of designing a generic effect inference algorithm that supports a variety of effect systems. In particular, I considered what algebraic structure and computational operations an effect system must provide to support a generic inference algorithm for higher-order recursive programs. Then I designed an effect inference algorithm that is parameterized over any effect systems that admits the algebraic structure. I mechanized the framework in Rocq and proved soundness, completeness, and bounds on the unresolved effects.

Advisor: Ethan Cecchetti

Non-Interactive Zero Knowledge Proofs (NIZKPs) is a cryptographic technique that allows a prover to demonstrate certain properties about the values the prover holds without revealing other information and without real-time interaction between the prover and the verifier. Refinement types are ordinary types further constrained by a logical property (such as {x: Int | x is even} representing the type of integers which are even). This project is a part of a Rahul's broader work on integrating NIZKPs (which allows us to demonstrate properties) and refinement types (which allows properties to exist as a part of the type system). In particular, I'm focusing on extending ideas from Liquid Types to support useful specifications about NIZKPs while preserving decidable refinement checking.

Advisor: Dmitriy Traytel

Incorrectness typing provides a way to reason what a program cannot type as, in addition to only what it can type as. I mechanized the first main theorem of a paper on incorrectness typing in Isabelle/HOL. Much of the work involved reconstructing informal arguments, resolving inconsistent notation, and identifying missing assumptions in intermediate lemmas. The resulting formalization establishes the theorem with machine-checked proofs.

Advisor: Fritz Henglein, James Avery

As a part of a final project for the a course, we explored classical simulation of Grover's quantum search algorithm using compact tensor representations of quantum states. We represented large tensors by decomposing them into sums of products of smaller tensors and studied how their representation complexity changes under rewriting. I proved that, for boolean satisfiability problems expressed in algebraic normal form, the representation complexity cannot increase after the first Grover iteration under our rewriting system. I also characterized the possible growth in the first iteration using the union closure of the boolean formula's terms and collaborated on a Haskell implementation of the simulator.

Advisor: Pál Zsámbok

Unit-distance graphs connect pairs of points in the plane that are exactly one unit apart. I explored optimization-based machine-learning methods for finding dense unit-distance graphs. I observed that conventional loss functions that aggregates distance-error objectives using L₁ or L₂ norms often concentrated optimization on a small number of edges. To correct for that, I experimented with L_p (quasi)norms with p < 1 to encourage the formation of multiple edges.