rstatics1.abs
conforms.abs
link2_0.art
subred.aux.art
subred.art

Proofs

Some quick notes:
".abs" files are abstracts, which act as specifications.
".art" files are proof documents that get checked by DECALRE.
Not all of the hypertext links work, particularly in the proof files. I'm working on this, but it's not a high priority.
The proofs are developed as follows:
Correlating the two:
rstatics.abs - Types for runtime terms.
conforms.abs - Conformance invariants and crucial lemmas that these are preserved by heap allocation and heap/frame update. The proofs are in conforms.art.
link2_0.abs - Lemmas correlating method fetch and method types. The proofs are in link2_0.art.
subred.aux.abs - Lemmas about frame allocation (perhaps these shuld go in conforms.abs). The proofs are in subred.aux.art.
subred.art - The subject reduction proof.
The major proof (subject reduction) can be found in subred.art. You can follow the links of imported files to see the specifications that this proof depends on. Important lemmas are proved in conforms.art, wfenv.art, link2_0.art and subred.aux.art.