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