Benjamin Lerner

Recent papers

A full list of my papers can be found here.

We explore an extensible product line of type systems for JavaScript, and explain the engineering and ergonomic choices choices we made in designing this system.

We develop a static type system for analyzing Firefox extensions to detect potential code paths that persist data to disk while the browser is in private-browsing mode.

We develop a static type system for analyzing jQuery client code for query errors, where jQuery results may contain too many, too few, or simply the wrong page elements, leading to unintended runtime behavior.

We define a model of overlays that dynamically compose declarative UI fragments onto a base document, and define conflict detection algorithms over this model.

We present S5, a semantics for the strict mode of the ECMAScript 5.1 (JavaScript) programming language.

We define a concise, executable formal model of event behavior in the DOM, with high fidelity to the DOM specification.


  • TeJaS: A Family of Type Systems for JavaScript: My current research interests focus on understanding, designing semantics for, and analyzing the many languages and APIs involved in client-side web programming. In particular, we are looking at designing customized type systems for verifying specific properties of JavaScript code.
  • Web browser extension compatibility: Firefox’s rise in popularity can be largely attributed to its much-touted extensions, which offer versatility, convenience and relatively-low learning curves to amateur and expert coders alike. But with such customizability comes problems: many extensions fail to work properly when installed simultaneously. This project aims to provide a better programming model for extensions that can detect and perhaps correct these conflicts before they happen.

Previous work

  • Non-uniform parallelism on a GPGPU: As an internship at AT&T Research, I worked with Trevor Jim and Yitzhak Mandelbaum on accelerating parsers using a general purpose GPU and the CUDA framework.
  • Pure-Causal Atomicity: The goal of atomicity analyses is to verify that certain sections of code appear to execute atomically to all other threads. This project extends recent work on causal atomicity (a model-checking approach to verify atomicity using Petri nets) with abstract atomicity (a type-theoretic approach using purity to validate mode code patterns as atomic).
  • SEMINAL: I’m working with Dan Grossman to improve the quality of error messages given by compilers. In practice, these messages are often precise but cryptic, and generating them often complicates the compilers themselves (potentially introducing bugs). This project aims to separate the two aspects of error finding and reporting, and in the process make the compilers both simpler and more informative.
  • Yampa: As my senior project at Yale, I worked on proving algebraic properties of the embedding of Yampa in Haskell.


download vcard icon
Email (essential):
Location (likely):
Department of Computer Science, Office 309
Post (possible):
work Post-Doctoral Research Associate Brown University / Department of Computer Science / 115 Waterman Street, 4th floor / Providence, RI 02912-1910