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

• Various type-setting errors, and
• A semantic error: the E-Break-Break and Err-Break-Reduction rules were missing. Without E-Break-Break, the term (label x (break y (break x 1))) gets stuck. E-Break-Break is now in Figure 8 of the 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:

• Examples and test results from the paper
• Redex model
• Desugaring
• Type-checker that disables access to window.XMLHttpRequest

Section 4.3: safeLookup desugared into λ_JS

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