For a more technical introduction, see our ECOOP 2010 paper on LambdaJS:
coq/ contains our mechanized semantics in Coq. Tested with Coq 8.3 and 8.4 beta.
Redex/ contains our mechanized semantics in PLT Redex. Tested with Racket 5.2.
haskell/ contains an implementation of desugaring. Tested with GHC 7.0.4. This software uses packages available on Hackage.
DisableXHR/ contains an implementation of our safe-subset example. Tested with GHC 6.10.4. This tool requires the LambdaJS Haskell package to be built and installed first.
Semantics for ECMAScript 5
The code for S5 is also available: