λ_JS: A Tested Semantics for JavaScript

λ_JS is a tested operational semantics for JavaScript. It is designed to be amenable to proofs and a simple target language for tools. The core semantics is much smaller and simpler than the JavaScript specification (three pages vs. 180 pages). Several other research groups employ λ_JS to simplify their work.

A Tractable Reduction Semantics

λ_JS is factored into two components.

• A reduction semantics models JavaScript's essentials—prototype-based objects, first-class functions, and control operators. We mechanize the reduction semantics in the Coq Proof Assistant and PLT Redex. The reduction semantics is small—three pages— and therefore tractable. All out tools and theorems work over this reduction semantics instead of targeting JavaScript directly.
• A desugaring function models JavaScript's details—implicit type conversions, four kinds of loops, switch statements, broken class-like syntax, etc. We implement desugaring in 600 lines of Haskell (with 2,000 lines for the JavaScript environment). With the exception of the with statement, desugaring is compositional, which lets us lift theorems about λ_JS to JavaScript theorems.

This separation of essentials and details makes λ_JS a tractable target for tools and theorems.

Based on the JavaScript Specification

λ_JS unambiguously encodes the prose in the official JavaScript specification (ECMA-262).

let toObject = fun(x) .
  if typeof x === "undefined" then
    throw makeException("TypeError")
  else if x === null then
    throw makeException("TypeError")
  else if typeof x === "boolean" then
    ref { 
      "$proto": "$Boolean.prototype",
      "$class": "Boolean",
      "$value": x
    }
  else
    ...

Tested Against Real Web Browsers

JavaScript is a complex language with an informal specification that Web browsers sometimes wilfully ignore (e.g., V8). λ_JS needs to argue that it is an adequate JavaScript semantics. We could try to prove a correspondence between λ_JS and a direct semantics for JavaScript, but that begs the question: What is the semantics of JavaScript?

In practice, JavaScript is truly defined by its major implementations. Open-source Web browsers are accompanied by extensive JavaScript test suites. We use parts of these test suites to test our semantics.

Since we mechanize desugaring and the reduction semantics, we can desugar and then run JavaScript programs. We can run the same programs directly with a "real" JavaScript implementation. We then check if λ_JS produces exactly the same output.

We perform this experiment with Rhino, SpiderMonkey, and V8, using a fragment of the Mozilla JavaScript test suite. The experiment reveals differences between each implementation (Rhino, SpiderMonkey, and V8). λ_JS achieves fidelity with Rhino. We are confident that we can account for the differences with minor variations in desugaring while leaving the reduction semantics intact.

Other Users of λ_JS

Several other groups have built systems with λ_JS:

• David van Horn and Matt Might use λ_JS to build an analytic framework for JavaScript,
• Rodolfo Toledo and Éric Tanter use λ_JS to specify aspects for JavaScript,
• IBEX, from Microsoft Research, uses λ_JS for its JavaScript backend to produce verified Web browser extensions, and
• Seonghoon Kang and Sukyoung Ryu (KAIST) extend λ_JS to study JavaScript modules.

This website highlights several of our own projects that use λ_JS.

Code: How to Use λ_JS

λ_JS consists of several independent tools.

• A JavaScript parser and pretty-printer, written in Haskell.
• An implementation of desugaring, written in Haskell. The core desugaring function is in Desugar.hs.
• An executable reduction semantics, written in PLT Redex.
• An interpreter for λ_JS, written in Racket. The Redex semantics above are executable, but this interpreter is significantly faster.
• A machine-checked reduction semantics in Coq.

Looking Forward: Semantics for For ECMAScript 5

JavaScript is a moving target. λ_JS, developed in late 2009, does not support the new features of ECMAScript 5. We've developed an updated semantics for ECMAScript 5, which is more complete (e.g., supports eval) and has better test coverage.