src/HOL/README.html
author nipkow
Thu Aug 19 17:06:05 1999 +0200 (1999-08-19)
changeset 7291 8aa66ddc0bea
parent 7290 f1a37c379317
child 7303 96bc013c8987
permissions -rw-r--r--
new entriues.
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
     3 
     4 <H2>HOL: Higher-Order Logic</H2>
     5 
     6 This directory contains the ML sources of the Isabelle system for
     7 Higher-Order Logic.<P>
     8 
     9 There are several subdirectories with examples:
    10 <DL>
    11 <DT>ex
    12 <DD>general examples
    13 
    14 <DT>Auth
    15 <DD>a new approach to verifying authentication protocols 
    16 
    17 <DT>Hoare
    18 <DD>verification of imperative programs; verification conditions are
    19 generated automatically from pre/post conditions and loop invariants.
    20 
    21 <DT>IMP
    22 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    23 
    24 <DT>Induct
    25 <DD>examples of (co)inductive definitions
    26 
    27 <DT>Integ 
    28 <DD>a development of the integers including efficient integer
    29 calculations (part of the standard HOL environment)
    30 
    31 <DT>IOA
    32 <DD>a simple theory of Input/Output Automata
    33 
    34 <DT>Lambda
    35 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    36 
    37 <DT>Lex
    38 <DD>verification of a simple lexical analyzer generator
    39 
    40 <DT>MiniML
    41 <DD>formalization of type inference for the language Mini-ML
    42 
    43 <DT>Real 
    44 <DD>a development of the reals and hyper-reals, which are used in
    45 non-standard analysis.  Also includes the positive rationals.  Used to build
    46 the image HOL-Real.
    47 
    48 <DT>Subst
    49 <DD>defines a theory of substitution and unification.
    50 
    51 <DT>TLA
    52 <DD>Lamport's Temporal Logic of Actions
    53 
    54 <DT>Tools
    55 <DD>holds code used to provide support for records, datatypes, induction, etc.
    56 
    57 <DT>UNITY
    58 <DD>Chandy and Misra's UNITY formalism.
    59 
    60 <DT>W0
    61 <DD>a precursor of MiniML, without let-expressions
    62 </DL>
    63 
    64 Useful references on Higher-Order Logic:
    65 
    66 <UL>
    67 
    68 <LI> P. B. Andrews,<BR>
    69     An Introduction to Mathematical Logic and Type Theory<BR>
    70     (Academic Press, 1986).
    71 
    72 <P>
    73 
    74 <LI> A. Church,<BR>
    75     A Formulation of the Simple Theory of Types<BR>
    76     (Journal of Symbolic Logic, 1940).
    77 
    78 <P>
    79 
    80 <LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
    81     Introduction to HOL: A theorem proving environment for higher order logic<BR>
    82     (Cambridge University Press, 1993).
    83 
    84 <P>
    85 
    86 <LI> J. Lambek and P. J. Scott,<BR>
    87     Introduction to Higher Order Categorical Logic<BR>
    88     (Cambridge University Press, 1986).
    89 
    90 </UL>
    91 
    92 </BODY></HTML>