Paper (October 3, 2015): This revision fixes the following errors in the ECOOP 2010 paper.
(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.
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