Various little changes like cmethd -> method and cfield -> field.
<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 on Micro
Java is in preparation. Until it has appeared, please consult the Bali home
page for publications.
</BODY>
</HTML>