ANNOUNCE
changeset 10162 947b7b8b0a69
parent 10161 4a3cd038aff8
child 10165 eb69823db997
     1.1 --- a/ANNOUNCE	Fri Oct 06 15:15:19 2000 +0200
     1.2 +++ b/ANNOUNCE	Fri Oct 06 16:11:53 2000 +0200
     1.3 @@ -30,6 +30,10 @@
     1.4      virtual machine and a specification of its bytecode verifier and a
     1.5      lightweight bytecode verifier, including proofs of type-safety.
     1.6  
     1.7 +  * HOL/BCV (Tobias Nipkow)
     1.8 +    Generic model of bytecode verification, i.e. data-flow
     1.9 +    analysis for assembly languages with subtypes.
    1.10 +
    1.11    * HOL/Real (Jacques Fleuriot)
    1.12      More on nonstandard real analysis.
    1.13