Projects

I co-lead the research team developing tracked capabilities in Scala 3’s production compiler. Capture checking adds opt-in effect tracking for stronger compile-time resource safety while preserving backwards compatibility. We have already capture-checked most of the standard library without invasive changes.

Capability classification lets types express which kinds of capabilities a value must not capture. Separation checking and mutation tracking build on capture checking to add Rust-like static control over resource sharing and lifetimes.

Reachability types give higher-order functional programs a form of ownership and aliasing control that works naturally with closures and first-class functions. The key idea is that a type’s reachability set records which heap locations a value can transitively access, enabling the type system to reason about separation between mutable values. Logical-relations models support proofs of effect safety and program equivalence.

I co-developed reachability types and led the Rocq mechanization.

A graph-based compiler IR for higher-order languages with mutable state, implemented in the Scala LMS compiler framework. Reachability types make aliasing and effect dependencies explicit in the graph, supporting optimizations across function calls. The formal metatheory includes a safety theorem and contextual equivalence results for the IR.

The call stack is fast and GC-free, but traditional semantics pop it immediately on function return, preventing stack-allocated data from outliving the current call. What if we don’t pop the stack right away? This approach, delayed popping, safely extends what can live on the stack to include variable-size data structures and closures, without moving them to the heap. 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. Controlling which resources they can access is one part of making them safe. This project applies Scala 3’s capability type system to check agents’ access to resources. 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.

A follow-up project funded by the Cyber-Defence Campus builds a prototype capability-safe coding agent for cyber defense.

LACUNA lets a program delegate parts of its implementation to an LLM. When execution reaches a typed hole, agent[T](task), the model generates code of type T using the capabilities available at that point in the program. The compiler checks the code before execution and returns errors to the model for revision.

Generated code can contain further agent holes, so agents can write their own control flow and delegate subtasks within the same program. Type and capability checks apply to each generated fragment.

Correlating asynchronous event streams requires choosing when and how to combine events. 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, allowing correlation strategies to be combined. 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 are often spread across several configuration languages. 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 challenging.

Starting from a definitional interpreter and applying staging and algebraic effects, we derive a correct-by-construction engine that outperforms KLEE by 4× on real-world code.

After a small code change, a type checker should be able to reuse most of its previous work. This project explores how to derive such incremental type checkers systematically, to reduce IDE latency and compilation times. It uses co-contextual typing rules, which let parts of a program be checked independently and their results combined.