Projects

What if a mainstream programming language could statically reason about effects, resource lifetimes, aliasing, and concurrency safety, without sacrificing expressiveness or forcing a Rust-style programming model on its users? That is the long-term agenda of this line of work, pursued in the context of Scala 3. The language is a real target with a large standard library, existing idioms, and a compiler that has to keep working. Getting the theory right and making it work in a real language are both hard problems, and both matter.

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 was instrumental in the first wave of this research, leading the mechanization effort in Rocq and contributing to the semantic foundations via logical relations, which establish stronger correctness properties including 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, enabling interprocedural optimizations that were previously off-limits for impure functional languages.

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. Beyond memory efficiency, it resolves a composability limitation of second-class values: they can now be returned and curried, resolving what was seen as a fundamental constraint.

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

LLM-based agents routinely invoke tools with real-world consequences: reading files, querying databases, sending 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.

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 is a powerful technique for finding bugs automatically: rather than running a program on one fixed input, it explores many execution paths simultaneously, using an SMT solver to check conditions along the way. Building such a tool 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.