| author | nipkow |
| Thu, 11 Nov 1999 12:44:08 +0100 | |
| changeset 8013 | 12f0ab3806c0 |
| child 8202 | f32931b93686 |
| permissions | -rw-r--r-- |
| nipkow@8013 | 1 |
<HTML><HEAD><TITLE>HOL/MicroJava/README</TITLE></HEAD> |
| nipkow@8013 | 2 |
<BODY> |
| nipkow@8013 | 3 |
|
| nipkow@8013 | 4 |
<H1>Micro Java</H1> |
| nipkow@8013 | 5 |
|
| nipkow@8013 | 6 |
This theory defines Micro Java, a small fragment of the programming language |
| nipkow@8013 | 7 |
Java (essentially just classes), together with a corresponding virtual |
| nipkow@8013 | 8 |
machine and a specification of its bytecode verifier. It is shown that Micro |
| nipkow@8013 | 9 |
Java and the given specification of the bytecode verifier are type safe. |
| nipkow@8013 | 10 |
Directories: |
| nipkow@8013 | 11 |
<DL> |
| nipkow@8013 | 12 |
<DT>J |
| nipkow@8013 | 13 |
<DD>Micro Java |
| nipkow@8013 | 14 |
|
| nipkow@8013 | 15 |
<DT>JVM |
| nipkow@8013 | 16 |
<DD>The virtual machine |
| nipkow@8013 | 17 |
|
| nipkow@8013 | 18 |
<DT>BV |
| nipkow@8013 | 19 |
<DD>The bytecode verifier |
| nipkow@8013 | 20 |
|
| nipkow@8013 | 21 |
</DL> |
| nipkow@8013 | 22 |
|
| nipkow@8013 | 23 |
<P> |
| nipkow@8013 | 24 |
The theory was developed by David von Oheimb, Cornelia Pusch and Tobias |
| nipkow@8013 | 25 |
Nipkow as part of the DFG-funded project |
| nipkow@8013 | 26 |
<a href="http://isabelle.in.tum.de/bali/">Bali</a>. A publication on Micro |
| nipkow@8013 | 27 |
Java is in preparation. Until it has appeared, please consult the Bali home |
| nipkow@8013 | 28 |
page for publications. |
| nipkow@8013 | 29 |
</BODY> |
| nipkow@8013 | 30 |
</HTML> |