src/HOL/README.html
author paulson
Thu Aug 19 16:54:38 1999 +0200 (1999-08-19)
changeset 7290 f1a37c379317
parent 4622 85aae356570c
child 7291 8aa66ddc0bea
permissions -rw-r--r--
updated
     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>IMP
    18 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    19 
    20 <DT>Induct
    21 <DD>examples of (co)inductive definitions
    22 
    23 <DT>Integ 
    24 <DD>a development of the integers including efficient integer
    25 calculations (part of the standard HOL environment)
    26 
    27 <DT>IOA
    28 <DD>extended example of Input/Output Automata
    29 
    30 <DT>Lambda
    31 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    32 
    33 <DT>Real 
    34 <DD>a development of the reals and hyper-reals, which are used in
    35 non-standard analysis.  Also includes the positive rationals.  Used to build
    36 the image HOL-Real.
    37 
    38 <DT>Subst
    39 <DD>defines a theory of substitution and unification.
    40 
    41 <DT>Tools
    42 <DD>holds code used to provide support for records, datatypes, induction, etc.
    43 
    44 <DT>UNITY
    45 <DD>Chandy and Misra's UNITY formalism.
    46 </DL>
    47 
    48 Useful references on Higher-Order Logic:
    49 
    50 <UL>
    51 
    52 <LI> P. B. Andrews,<BR>
    53     An Introduction to Mathematical Logic and Type Theory<BR>
    54     (Academic Press, 1986).
    55 
    56 <P>
    57 
    58 <LI> A. Church,<BR>
    59     A Formulation of the Simple Theory of Types<BR>
    60     (Journal of Symbolic Logic, 1940).
    61 
    62 <P>
    63 
    64 <LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
    65     Introduction to HOL: A theorem proving environment for higher order logic<BR>
    66     (Cambridge University Press, 1993).
    67 
    68 <P>
    69 
    70 <LI> J. Lambek and P. J. Scott,<BR>
    71     Introduction to Higher Order Categorical Logic<BR>
    72     (Cambridge University Press, 1986).
    73 
    74 </UL>
    75 
    76 </BODY></HTML>