new entriues.
authornipkow
Thu Aug 19 17:06:05 1999 +0200 (1999-08-19)
changeset 72918aa66ddc0bea
parent 7290 f1a37c379317
child 7292 dff3470c5c62
new entriues.
src/HOL/README.html
     1.1 --- a/src/HOL/README.html	Thu Aug 19 16:54:38 1999 +0200
     1.2 +++ b/src/HOL/README.html	Thu Aug 19 17:06:05 1999 +0200
     1.3 @@ -14,6 +14,10 @@
     1.4  <DT>Auth
     1.5  <DD>a new approach to verifying authentication protocols 
     1.6  
     1.7 +<DT>Hoare
     1.8 +<DD>verification of imperative programs; verification conditions are
     1.9 +generated automatically from pre/post conditions and loop invariants.
    1.10 +
    1.11  <DT>IMP
    1.12  <DD>mechanization of a large part of a semantics text by Glynn Winskel
    1.13  
    1.14 @@ -25,11 +29,17 @@
    1.15  calculations (part of the standard HOL environment)
    1.16  
    1.17  <DT>IOA
    1.18 -<DD>extended example of Input/Output Automata
    1.19 +<DD>a simple theory of Input/Output Automata
    1.20  
    1.21  <DT>Lambda
    1.22  <DD>a proof of the Church-Rosser theorem for lambda-calculus
    1.23  
    1.24 +<DT>Lex
    1.25 +<DD>verification of a simple lexical analyzer generator
    1.26 +
    1.27 +<DT>MiniML
    1.28 +<DD>formalization of type inference for the language Mini-ML
    1.29 +
    1.30  <DT>Real 
    1.31  <DD>a development of the reals and hyper-reals, which are used in
    1.32  non-standard analysis.  Also includes the positive rationals.  Used to build
    1.33 @@ -38,11 +48,17 @@
    1.34  <DT>Subst
    1.35  <DD>defines a theory of substitution and unification.
    1.36  
    1.37 +<DT>TLA
    1.38 +<DD>Lamport's Temporal Logic of Actions
    1.39 +
    1.40  <DT>Tools
    1.41  <DD>holds code used to provide support for records, datatypes, induction, etc.
    1.42  
    1.43  <DT>UNITY
    1.44  <DD>Chandy and Misra's UNITY formalism.
    1.45 +
    1.46 +<DT>W0
    1.47 +<DD>a precursor of MiniML, without let-expressions
    1.48  </DL>
    1.49  
    1.50  Useful references on Higher-Order Logic: