src/HOL/MicroJava/README.html
changeset 10086 5245fa2ca8d3
parent 10085 a9704bf90031
child 10087 4dc7edfb0b5f
equal deleted inserted replaced
10085:a9704bf90031 10086:5245fa2ca8d3
     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 is
       
    27 <a href="http://isabelle.in.tum.de/Bali/papers/MOD99.html">available</a>.
       
    28 </BODY>
       
    29 </HTML>