src/HOL/README.html
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 4622 85aae356570c
child 7290 f1a37c379317
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 theory of the integers including efficient integer calculations
    25 
    26 <DT>IOA
    27 <DD>extended example of Input/Output Automata
    28 
    29 <DT>Lambda
    30 <DD>a proof of the Church-Rosser theorem for lambda-calculus
    31 
    32 <DT>Subst
    33 <DD>subdirectory defining a theory of substitution and unification.
    34 </DL>
    35 
    36 Useful references on Higher-Order Logic:
    37 
    38 <UL>
    39 
    40 <LI> P. B. Andrews,<BR>
    41     An Introduction to Mathematical Logic and Type Theory<BR>
    42     (Academic Press, 1986).
    43 
    44 <P>
    45 
    46 <LI> A. Church,<BR>
    47     A Formulation of the Simple Theory of Types<BR>
    48     (Journal of Symbolic Logic, 1940).
    49 
    50 <P>
    51 
    52 <LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
    53     Introduction to HOL: A theorem proving environment for higher order logic<BR>
    54     (Cambridge University Press, 1993).
    55 
    56 <P>
    57 
    58 <LI> J. Lambek and P. J. Scott,<BR>
    59     Introduction to Higher Order Categorical Logic<BR>
    60     (Cambridge University Press, 1986).
    61 
    62 </UL>
    63 
    64 </BODY></HTML>