1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/MicroJava/README.html Thu Nov 11 12:44:08 1999 +0100
1.3 @@ -0,0 +1,30 @@
1.4 +<HTML><HEAD><TITLE>HOL/MicroJava/README</TITLE></HEAD>
1.5 +<BODY>
1.6 +
1.7 +<H1>Micro Java</H1>
1.8 +
1.9 +This theory defines Micro Java, a small fragment of the programming language
1.10 +Java (essentially just classes), together with a corresponding virtual
1.11 +machine and a specification of its bytecode verifier. It is shown that Micro
1.12 +Java and the given specification of the bytecode verifier are type safe.
1.13 +Directories:
1.14 +<DL>
1.15 +<DT>J
1.16 +<DD>Micro Java
1.17 +
1.18 +<DT>JVM
1.19 +<DD>The virtual machine
1.20 +
1.21 +<DT>BV
1.22 +<DD>The bytecode verifier
1.23 +
1.24 +</DL>
1.25 +
1.26 +<P>
1.27 +The theory was developed by David von Oheimb, Cornelia Pusch and Tobias
1.28 +Nipkow as part of the DFG-funded project
1.29 +<a href="http://isabelle.in.tum.de/bali/">Bali</a>. A publication on Micro
1.30 +Java is in preparation. Until it has appeared, please consult the Bali home
1.31 +page for publications.
1.32 +</BODY>
1.33 +</HTML>