λJS: The Essence of JavaScript
Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi

Paper (October 3, 2015): This revision fixes the following errors in the ECOOP 2010 paper.

Thanks to Ben Lerner, David Van Horn, Jean-Baptiste Jeannin, Rodolfo Toledo, and Jan Vitek and his students, for catching these.

Download the published paper. (The Essence of JavaScript. ECOOP 2010.)

Tools, Tests, and Mechanized Semantics: Source code and instructions (packaged on 2009-12-14)

The latest source code is available online.

Some interesting files:

Section 4.3: safeLookup desugared into λJS

Section 4.2: Proof details for safety and subjection reduction for the type system