HOL/MicroJava;
authorwenzelm
Tue Sep 26 17:03:52 2000 +0200 (2000-09-26)
changeset 100808fb8c17d1cb5
parent 10079 0d78784176f4
child 10081 352412857003
HOL/MicroJava;
NEWS
     1.1 --- a/NEWS	Tue Sep 26 17:02:51 2000 +0200
     1.2 +++ b/NEWS	Tue Sep 26 17:03:52 2000 +0200
     1.3 @@ -225,6 +225,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/MicroJava: formalization of a fragment of Java, together with a
     1.8 +corresponding virtual machine and a specification of its bytecode
     1.9 +verifier and a lightweight bytecode verifier, including proofs of
    1.10 +type-safety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    1.11 +Cornelia Pusch (see also the homepage of project Bali at
    1.12 +http://isabelle.in.tum.de/Bali/);
    1.13 +
    1.14  * HOL/Algebra: new theory of rings and univariate polynomials, by
    1.15  Clemens Ballarin;
    1.16