<HTML><HEAD><TITLE>HOL/MicroJava/README</TITLE></HEAD>
<BODY>
<H1>Micro Java</H1>
This theory defines Micro Java, a small fragment of the programming language
Java (essentially just classes), together with a corresponding virtual
machine and a specification of its bytecode verifier. It is shown that Micro
Java and the given specification of the bytecode verifier are type safe.
Directories:
<DL>
<DT>J
<DD>Micro Java
<DT>JVM
<DD>The virtual machine
<DT>BV
<DD>The bytecode verifier
</DL>
<P>
The theory was developed by David von Oheimb, Cornelia Pusch and Tobias
Nipkow as part of the DFG-funded project
<a href="http://isabelle.in.tum.de/bali/">Bali</a>. A publication is
<a href="http://isabelle.in.tum.de/Bali/papers/MOD99.html">available</a>.
</BODY>
</HTML>