Projects

Modern programming languages are increasingly tracking substructural properties, such as ownership, object lifetimes, linearity, and borrowing, with Rust being one of the most prominent implementations. However, prior research in this space mostly focuses on objects and classes, and it is far less concerned with higher-order functions. Enter reachability types: a novel take on substructural properties specifically tailored to imperative higher-order functional programming. The type system builds on a simple substrate derived from separation logic, and features a notion of lightweight reachability polymorphism, which arguably makes the type system ergonomic.

I am part of the core team behind reachability types, and leading the mechanization effort of the base system + future extensions in Coq. We intend to scale the type system to the features of full-blown functional languages and strive for end-to-end mechanized artifacts at each stage of development.

Also, I have a leading role in marrying reachability types with effect systems to create a new graph-based intermediate representation (IR) for compiling impure functional languages like Scala and OCaml. Effects and reachability overcome long-standing issues that limit the scope of graph-based optimizations for these kinds of languages to single functions (think “Sea-of-nodes” IRs as in TurboFan). Our typed graph IR based on concepts from separation logic unlocks truly interprocedural optimizations.

The IR is being developed in the Scala LMS compiler framework. You can try out an early interactive prototype in your Browser.

I have been working on making symbolic execution easy, scalable, and performant using PL principles and code generation techniques.

Symbolic execution (SE) is a popular software-testing technique from the 1970s, e.g., used for bug finding, security, verification, and program synthesis. The underlying idea is to simultaneously explore multiple execution paths in a given program, with some inputs being left symbolic rather than concrete, and generating constraints checked by SMT solvers.

However, building an SE engine is often considered “the most difficult aspect of creating solver-aided tools”. Our work drastically reduces this hardship by a streamlined process which is both easy to grasp and performant. It reconciles the strengths of prevailing construction approaches for SE without their downsides, i.e., those based on interpreters (high level, but slow) and instrumentation of programs (performant, but ad hoc, language-specific, and hard to generalize).

Our framework relies heavily on concepts from functional programming, i.e., the interpreters return a monadic representation of symbolic programs in terms of algebraic effects and handlers. Effect handlers grant extensibility (new object-language effects can be added), and customizability (effects can be denoted differently on the fly). For instance, SMT solver interactions can be abstracted over with a dedicated algebraic effect, and concrete handlers implement the communication between the solver (e.g., Z3) and the SE engine. Exploring different execution paths is a nondeterminism effect, and concrete handlers implement user-defined search strategies and heuristics. To eliminate all abstraction and interpretation overhead, we exploit an old discovery by Futamura showing how a compiler can be mechanically derived from an interpreter using partial evaluation/multi-stage programming.

The extensible framework in principle applies to any kind of symbolic execution. So far, we have evaluated it by the example of “all-path symbolic execution” of LLVM IR programs, and other flavors are planned in the future. Remarkably, the first version [Wei et al. 2020] with a naive code generation backend already outperforms the interpreter-based KLEE by up to 2x. Since then, we have further improved performance by generating code for asynchronous path exploration [Wei et al. 2021], followed by compiling truly parallel explorations [Wei et al. 2023] . We now achieve average speedups of 4x over KLEE on real-world code bases (e.g., GNU Coreutils).

The call stack was first proposed by Dijkstra for the ALGOL language in the 1960s, and it was a breakthrough that enabled programming with recursive functions. Since then, “the stack” with its simple and yet very rigid automatic memory allocation/reclamation has been the backbone of most programming language implementations (with a few notable exceptions, such as Standard ML). That the stack immediately “pops” when a function returns is taught in every CS curriculum and unquestioningly accepted.

However, “what if we don’t pop the stack”? A simple question with profound consequences: If we let the stack frame live “just a little longer” than usual, we gain the ability to return data structures of variable size entirely on the stack! We can run a much larger class of computations purely on the stack, requiring no heap, no GC, no manual memory management whatsoever. This is beneficial for a wide range of applications, especially those which process short-lived ephemeral data, e.g., reactive and dataflow computations, differential programming, HTTP servers, etc.

Several languages (e.g., C#, Swift, and OCaml) have recently proposed adding support for stack-allocated values. Those proposals, while promising, have limitations, e.g., the size of stack-allocated data has to be fully known at compile time, which limits expressiveness of on-stack computations and inhibits uses of higher-order functions. In contrast, our approach is much more seamless and supports returning on-stack data of statically unknown size, including anonymous function closures.

To ensure delayed stack allocation is safe, we also contribute an expressive type system tracking the storage mode of expressions (i.e., heap and stack) and supporting forms of storage-mode polymorphic code. We proved type-and-memory safety of our type system in Coq, and have implemented a prototype compiler on top of Scala native. Our benchmarks show that the approach can reduce garbage collection overhead by up to 54% and can improve wall-clock time by up to 22%.

Last, but not least, delayed popping grants more design freedom and expressiveness when programming with second-class values. These play a central role for programming effects and capabilities. A perceived limitation of the initial work was the inability to return second-class values, precisely because they have a stack-bounded life time and the traditional stack semantics was followed. That prevents currying lists of second-class parameters, and makes them far less composable than they should be. The delayed popping strategy in this work gives a particularly simple and straightforward solution to the problem, to the point that it appears almost trivial. All it took was breaking with a 60 year old convention.

Cartesius is a semantic model for defining expressive n-way joins/merges over asynchronous event sequences/streams. Joins exists in different domains, e.g., stream-relational algebra, complex event patterns, (functional) reactive programming and concurrent programming (join calculus). With Cartesius, we can define join variants in a uniform and structured manner. We may think of Cartesius as solving an instance of Wadler’s “expression problem” in the realm of big data. The workhorse are algebraic effects and handlers, which we employ to interpret declarative join pattern specifications in different ways.

PolyJoin complements Cartesius with a pragmatic, type-safe, and purely combinator-based programming language embedding of comprehension syntax for joins. It permits more liberal notions of computations than LINQ, respectively monadic “do” and “for” comprehensions.

Coq and Agda developments on the dependent object types (DOT) family of calculi, the foundation of the Scala programming language. I explore pathways to bring richer forms of dependent types into the language. Occasionally, I also contribute to Tiark Rompf’s minidot repository.