@Article{Klein:TOPLAS-28-4-619,
  author =       "Gerwin Klein and Tobias Nipkow",
  title =        "A Machine-Checked Model for a {Java}-Like Language,
                 Virtual Machine, and Compiler",
  journal =      "ACM Transactions on Programming Languages and Systems",
  volume =       "28",
  number =       "4",
  year =         "2006",
  pages =        "619--695",
  ee =           "http://doi.acm.org/10.1145/1146811",
}