VLDB 2026 Research / reviewers in the wild / expert
Stephen Dolan
dblp:125/7554
· DBLP profile ↗
14ranked-venue papers
6as first author
6since 2021 · last 2025
—ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 11 · 4 first-author · 6 since 2021Systems, architecture and hardware · 2 · 2 first-authorApplied, interdisciplinary, general and emerging computing · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Lifetime Dispersion and Generational GC: An Intellectual AbstractabstractThe effectiveness of generational garbage collection is usually explained through the generational hypothesis, that “most objects die young”. Stephen Dolan |
ISMM | 1 |
| 2025 | Data Race Freedom à la ModeabstractWe present DRFCaml, an extension of OCaml’s type system that guarantees data race freedom for multithreaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et al., who extend OCaml with modes that keep track of locality, uniqueness, and affinity. We introduce two new mode axes, contention and portability , which record whether data has been shared or can be shared between multiple threads. Although this basic type-and-mode system has limited expressive power by itself, it does let us express APIs for capsules , regions of memory whose access is controlled by a unique ghost key, and reader-writer locks , which allow a thread to safely acquire partial or full ownership of a key. We show that this allows complex data structures (which may involve aliasing and mutable state) to be safely shared between threads. We formalize the complete system and establish its soundness by building a semantic model of it in the Iris program logic on top of the Rocq proof assistant. Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer |
Proc. ACM Program. Lang. | 5 |
| 2025 | Modal Effect TypesabstractEffect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types. Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen |
Proc. ACM Program. Lang. | 3 |
| 2024 | Unboxed Data Constructors: Or, How cpp Decides a Halting ProblemabstractWe propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusion, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes. Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order λ -calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our algorithm turns out to be closely related to the normalization strategy for macro expansion in the cpp preprocessor. Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop |
Proc. ACM Program. Lang. | 2 |
| 2024 | Oxidizing OCaml with Modal Memory ManagementabstractProgrammers can often improve the performance of their programs by reducing heap allocations: either by allocating on the stack or reusing existing memory in-place. However, without safety guarantees, these optimizations can easily lead to use-after-free errors and even type unsoundness. In this paper, we present a design based on modes which allows programmers to safely reduce allocations by using stack allocation and in-place updates of immutable structures. We focus on three mode axes: affinity, uniqueness and locality. Modes are fully backwards compatible with existing OCaml code and can be completely inferred. Our work makes manual memory management in OCaml safe and convenient and charts a path towards bringing the benefits of Rust to OCaml. Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley |
Proc. ACM Program. Lang. | 3 |
| 2021 | Retrofitting effect handlers onto OCamlabstractEffect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. We present a design and evaluate a full-fledged efficient implementation of effect handlers for OCaml, an industrial-strength multi-paradigm programming language. Our implementation strives to maintain the backwards compatibility and performance profile of existing OCaml code. Retrofitting effect handlers onto OCaml is challenging since OCaml does not currently have any non-local control flow mechanisms other than exceptions. Our implementation of effect handlers for OCaml: (i) imposes a mean 1% overhead on a comprehensive macro benchmark suite that does not use effect handlers; (ii) remains compatible with program analysis tools that inspect the stack; and (iii) is efficient for new code that makes use of effect handlers. K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Anil Madhavapeddy |
PLDI | 2 |
| 2020 | Repairing and mechanising the JavaScript relaxed memory modelabstractModern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the JavaScript specification defines an axiomatic relaxed memory model to describe their behaviour. While this model is heavily based on the C/C++11 model, it diverges in some key areas. JavaScript chooses to give a well-defined semantics to data-races, unlike the "undefined behaviour" of C/C++11. Moreover, the JavaScript model is mixed-size. This means that its accesses are not to discrete locations, but to (possibly overlapping) ranges of bytes. Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-yu Guo |
PLDI | 5 |
| 2020 | Brief Announcement: The Only Undoable CRDTs are CountersabstractIn comparing well-known CRDTs representing sets that can grow and shrink, we find caveats. In one, the removal of an element cannot be reliably undone. In another, undesirable states are attainable, such as when an element is present -1 times (and so must be added for the set to become empty). The first lacks a general-purpose undo, while the second acts less like a set and more like a tuple of counters, one per possible element. Stephen Dolan |
PODC | 1 |
| 2020 | Retrofitting parallelism onto OCamlabstractOCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors. K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Anmol Sahoo, Sudha Parimala, Atul Dhiman, Anil Madhavapeddy |
Proc. ACM Program. Lang. | 2 |
| 2018 | Bounding data races in space and timeabstractWe propose a new semantics for shared-memory parallel programs that gives strong guarantees even in the presence of data races. Our local data race freedom property guarantees that all data-race-free portions of programs exhibit sequential semantics. We provide a straightforward operational semantics and an equivalent axiomatic model, and evaluate an implementation for the OCaml programming language. Our evaluation demonstrates that it is possible to balance a comprehensible memory model with a reasonable (no overhead on x86, ~0.6% on ARM) sequential performance trade-off in a mainstream programming language. Stephen Dolan, K. C. Sivaramakrishnan, Anil Madhavapeddy |
PLDI | 1 |
| 2017 | Polymorphism, subtyping, and type inference in MLsubabstractWe present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict superset of core ML programs. Stephen Dolan, Alan Mycroft |
POPL | 1 |
| 2017 | Transcriptomics technologiesabstractTranscriptomics technologies are the techniques used to study an organism's transcriptome, the sum of all of its RNA transcripts.The information content of an organism is recorded in the DNA of its genome and expressed through transcription.Here, mRNA serves as a transient intermediary molecule in the information network, whilst noncoding RNAs perform additional diverse functions.A transcriptome captures a snapshot in time of the total transcripts present in a cell.The first attempts to study the whole transcriptome began in the early 1990s, and technological advances since the late 1990s have made transcriptomics a widespread discipline.Transcriptomics has been defined by repeated technological innovations that transform the field.There are two key contemporary techniques in the field: microarrays, which quantify a set of predetermined sequences, and RNA sequencing (RNA-Seq), which uses high- throughput sequencing to capture all sequences.Measuring the expression of an organism's genes in different tissues, conditions, or time points gives information on how genes are regulated and reveals details of an organism's biology.It can also help to infer the functions of previously unannotated genes.Transcriptomic analysis has enabled the study of how gene expression changes in different organisms and has been instrumental in the understanding of human disease.An analysis of gene expression in its entirety allows detection of broad coordinated trends which cannot be discerned by more targeted assays.This is a "Topic Page" article for PLOS Computational Biology. HistoryTranscriptomics has been characterised by the development of new techniques which have redefined what is possible every decade or so and render previous technologies obsolete (Fig 1).The first attempt at capturing a partial human transcriptome was published in 1991 and Rohan Lowe, Neil J. Shirley, Mark Bleackley, Stephen Dolan, Thomas Shafee |
PLoS Comput. Biol. | 4 |
| 2013 | Fun with semirings: a functional pearl on the abuse of linear algebraabstractDescribing a problem using classical linear algebra is a very well-known problem-solving technique. If your question can be formulated as a question about real or complex matrices, then the answer can often be found by standard techniques. Stephen Dolan |
ICFP | 1 |
| 2013 | Compiler support for lightweight context switchingabstractWe propose a new language-neutral primitive for the LLVM compiler, which provides efficient context switching and message passing between lightweight threads of control. The primitive, called Swapstack, can be used by any language implementation based on LLVM to build higher-level language structures such as continuations, coroutines, and lightweight threads. As part of adding the primitives to LLVM, we have also added compiler support for passing parameters across context switches. Our modified LLVM compiler produces highly efficient code through a combination of exposing the context switching code to existing compiler optimizations, and adding novel compiler optimizations to further reduce the cost of context switches. To demonstrate the generality and efficiency of our primitives, we add one-shot continuations to C++, and provide a simple fiber library that allows millions of fibers to run on multiple cores, with a work-stealing scheduler and fast inter-fiber sychronization. We argue that compiler-supported lightweight context switching can be significantly faster than using a library to switch between contexts, and provide experimental evidence to support the position. Stephen Dolan, Servesh Muralidharan, David Gregg |
ACM Trans. Archit. Code Optim. | 1 |