@techreport{KleinN04,
  author={Gerwin Klein and Tobias Nipkow},
  title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
  number={0400001T.1},
  institution={National ICT Australia},
  address={Sydney},
  month=mar,
  year=2004
}