http://www.cs.cornell.edu/~jnfoster/
This is an unofficial reimagining of the Archive of Formal Proofs
A Theory of Featherweight Java in Isabelle/HOLby J. Nathan Foster and Dimitrios Vytiniotis