ANNOUNCE
changeset 10162 947b7b8b0a69
parent 10161 4a3cd038aff8
child 10165 eb69823db997
equal deleted inserted replaced
10161:4a3cd038aff8 10162:947b7b8b0a69
    27   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    27   * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and
    28     Cornelia Pusch)
    28     Cornelia Pusch)
    29     Formalization of a fragment of Java, together with a corresponding
    29     Formalization of a fragment of Java, together with a corresponding
    30     virtual machine and a specification of its bytecode verifier and a
    30     virtual machine and a specification of its bytecode verifier and a
    31     lightweight bytecode verifier, including proofs of type-safety.
    31     lightweight bytecode verifier, including proofs of type-safety.
       
    32 
       
    33   * HOL/BCV (Tobias Nipkow)
       
    34     Generic model of bytecode verification, i.e. data-flow
       
    35     analysis for assembly languages with subtypes.
    32 
    36 
    33   * HOL/Real (Jacques Fleuriot)
    37   * HOL/Real (Jacques Fleuriot)
    34     More on nonstandard real analysis.
    38     More on nonstandard real analysis.
    35 
    39 
    36   * HOL/Algebra (Clemens Ballarin)
    40   * HOL/Algebra (Clemens Ballarin)