--- a/NEWS Mon May 12 14:16:38 2003 +0200
+++ b/NEWS Mon May 12 14:17:55 2003 +0200
@@ -174,12 +174,16 @@
* UNITY: added the Meier-Sanders theory of progress sets;
+* MicroJava: bytecode verifier and lightweight bytecode verifier
+as abstract algorithms, instantiated to the JVM;
+
* Bali: Java source language formalization. Type system, operational
semantics, axiomatic semantics. Supported language features:
classes, interfaces, objects,virtual methods, static methods,
static/instance fields, arrays, access modifiers, definite
assignment, exceptions.
+
*** ZF ***
* ZF/Constructible: consistency proof for AC (Gödel's constructible