λ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.

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).

Input Type Result
Undefined Throw a TypeError exception
Null Throw a TypeError exception
Boolean Create a new Boolean object whose [[value]] property is set tot he value of the boolean. See 15.6 for a description of Boolean objects.
etc.
Algorithm 9.9 from ECMA-262, 3rd ed.
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
    ...
Algorithm 9.9 encoded in λJS

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.

The λJS Testing Experiment

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:

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

Code: How to Use λJS

λJS consists of several independent tools.

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.