src/HOL/README.html
changeset 13852 dd2cd94a51e6
parent 10262 3c43e8086cba
child 14024 213dcc39358f
equal deleted inserted replaced
13851:f6923453953a 13852:dd2cd94a51e6
    63 
    63 
    64 <dt>Lattice
    64 <dt>Lattice
    65 <dd>lattices and order structures (in Isabelle/Isar)
    65 <dd>lattices and order structures (in Isabelle/Isar)
    66 
    66 
    67 <dt>Lex
    67 <dt>Lex
    68 <dd>verification of a simple lexical analyzer generator
    68 <dd>verification of a simple lexical analyser generator
    69 
    69 
    70 <dt>MicroJava
    70 <dt>MicroJava
    71 <dd>formalization of a fragment of Java, together with a corresponding
    71 <dd>formalization of a fragment of Java, together with a corresponding
    72 virtual machine and a specification of its bytecode verifier and a
    72 virtual machine and a specification of its bytecode verifier and a
    73 lightweight bytecode verifier, including proofs of type-safety.
    73 lightweight bytecode verifier, including proofs of type-safety.