Warning: This material has known errors, and is available for archival purposes only. Our ECOOP publication is a corrected version of λ_JS.

Download the paper: Brown CS TR CS-09-10

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

Latest source code.

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