Projects

Can a mainstream language statically reason about effects, resource lifetimes, aliasing, and concurrency safety, without forcing a Rust-style programming model on its users? This line of work pursues that question in Scala 3: a real language with a large standard library, existing idioms, and a compiler that has to keep working.

Reachability types give higher-order functional programs a form of ownership and aliasing control that works naturally with closures and first-class functions, unlike ownership systems designed around objects and classes. The key idea is that a type’s reachability set records which heap locations a value can transitively access, enabling the type system to enforce separation between aliased data without sacrificing expressiveness.

I led the Rocq mechanization during the first wave of this research and contributed to the semantic foundations via logical relations, which establish stronger correctness properties: effect safety and an equational theory that justifies compiler optimizations.

Compilers for languages with side effects, like Scala and OCaml, traditionally cannot optimize across function boundaries. Without precise knowledge of what each call might do to memory, the compiler has to assume the worst. Building on reachability types, our typed graph IR encodes effect and aliasing information directly in the IR’s dependency structure. This lets the compiler safely reorder, fuse, and eliminate computations across function calls.

The call stack is fast and GC-free, but traditional semantics pop it immediately on function return, limiting it to data of known size that doesn’t outlive the current call. What if we don’t pop the stack right away? This simple idea, delayed popping, safely extends what can live on the stack to include variable-size data structures and closures, requiring no heap allocation and no GC. It also removes a composability limitation of second-class values: they can now be returned and curried.

The approach reduces GC overhead by up to 54% and improves wall-clock time by up to 22% on real workloads.

LLM-based agents invoke tools that read files, query databases, and send requests. Ensuring they do only what they are supposed to do is an open problem. This project applies Scala 3’s capability type system as a static safety harness for agents. Capabilities are first-class values that must be explicitly threaded through code, so the type checker can verify that an agent cannot access resources it was never granted. We show that LLMs can generate capability-safe code that passes these checks without significant loss in task performance.

LLM agents increasingly act by writing code, but the runtime that drives the agent and the code the model writes remain separate: the runtime owns the loop, the context, and the control flow, so a model failure is contained to a single action. LACUNA closes this split without giving up the containment. Each agent action is a typed hole, agent[T](task), which the LLM fills with code when execution reaches it; the code is type-checked against the surrounding program before it runs. A rejected action leaves the environment untouched and its compiler diagnostics drive a retry, while the type check bounds which tools and data the action may use and how they flow. ReAct loops, sub-agents, skills, parallel decomposition, and multi-model planning become ordinary control flow.

Correlating asynchronous event streams in a general, composable way is harder than it looks. Stream databases, reactive programming frameworks, and join calculi all solve overlapping problems but with incompatible semantics.

Cartesius provides a unifying semantic framework: join patterns are expressed declaratively, and algebraic effect handlers determine how they are evaluated, making it easy to mix and match correlation strategies. PolyJoin turns this into a practical, type-safe language embedding.

Explores foundations of typed distributed programming with first-class server abstractions, join patterns for synchronization, and transparent placement. Server configurations, deployments, and cloud/middleware services can be programmed as libraries of combinators in CPL. These tasks usually require a multitude of unsafe configuration languages with no safety net. Comes with an interpreter in Scala and a PLT Redex mechanization.

Symbolic execution finds bugs automatically: rather than running a program on one fixed input, it explores many execution paths at once, using an SMT solver to check conditions along the way. Building such an engine correctly and efficiently is notoriously hard.

We show it doesn’t have to be. Starting from a clean definitional interpreter and applying staging and algebraic effects, we derive a correct-by-construction engine that outperforms KLEE by 4× on real-world code.

Explores how we may systematically obtain an incremental type checker for a given programming language. Incrementalization avoids expensive re-computation of type checking and other program analyses in large-scale software projects and thus may lower the latency in IDEs and decrease compilation times overall. The project is based on the notion of co-contextual typing rules.