Benjamin Lerner

Recent papers

A full list of my papers can be found here.

We try to combine the exploratory benefits of a REPL (Read-Eval-Print Loop) with the persistent contents of a typical program-definitions window, using the UI metaphor of a chat client.

Integrating computing into other subjects promises to address many challenges to offering standalone CS courses in K-12 contexts. Integrated curricula must be designed carefully, however, to both meet learning objectives of the host discipline and to gain traction with teachers. We describe the multi-year evolution of Bootstrap, a curriculum for integrating computing into middle- and high-school mathematics. We discuss the initial design and the various modifications we have made over the years to better support math instruction, leading to our goal of using integrated curricula to cover standards in both math and CS. We provide advice for others aiming for integration and raise questions for CS educators about how we might better support learning in other disciplines.

Modern systems consist of large numbers of languages, frameworks, libraries, APIs, and more. Each has characteristic behavior and data. Capturing these in semantics is valuable not only for understanding them but also essential for formal treatment (such as proofs). Unfortunately, most of these systems are defined primarily through implementations, which means the semantics needs to be \emph{learned}. We describe the problem of learning a semantics, provide a structuring process that is of potential value, and also outline our failed attempts at achieving this so far.

We revisit the World model of functional event-based programming and extract a new primitive, a Reactor, to enable programmatic control over these reactive programs.

We expand the space of programs that can be synthesized from templates, and attempt to apply it to derive desugaring transformations for constructs in a lambda calculus.

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.


  • Pyret: A language designed for teaching introductory programming, with an emphasis on testing, clarity, and the occasionally-awful pirate-themed pun.
  • 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):
West Village H, Office 326
Post (possible):
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
work Lecturer Office 326