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
paulson@2080
     1
<!-- $Id$ -->
wenzelm@3279
     2
<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
clasohm@1339
     3
wenzelm@3279
     4
<H2>HOL: Higher-Order Logic</H2>
clasohm@1339
     5
wenzelm@3279
     6
This directory contains the ML sources of the Isabelle system for
wenzelm@3279
     7
Higher-Order Logic.<P>
clasohm@1339
     8
wenzelm@3279
     9
There are several subdirectories with examples:
paulson@2080
    10
<DL>
clasohm@1339
    11
<DT>ex
paulson@2080
    12
<DD>general examples
paulson@2080
    13
paulson@2080
    14
<DT>Auth
paulson@2080
    15
<DD>a new approach to verifying authentication protocols 
paulson@2080
    16
paulson@2080
    17
<DT>IMP
paulson@2080
    18
<DD>mechanization of a large part of a semantics text by Glynn Winskel
paulson@2080
    19
paulson@3125
    20
<DT>Induct
paulson@3125
    21
<DD>examples of (co)inductive definitions
paulson@3125
    22
paulson@7290
    23
<DT>Integ 
paulson@7290
    24
<DD>a development of the integers including efficient integer
paulson@7290
    25
calculations (part of the standard HOL environment)
paulson@2080
    26
paulson@2080
    27
<DT>IOA
paulson@3125
    28
<DD>extended example of Input/Output Automata
paulson@2080
    29
paulson@2080
    30
<DT>Lambda
paulson@2080
    31
<DD>a proof of the Church-Rosser theorem for lambda-calculus
clasohm@1339
    32
paulson@7290
    33
<DT>Real 
paulson@7290
    34
<DD>a development of the reals and hyper-reals, which are used in
paulson@7290
    35
non-standard analysis.  Also includes the positive rationals.  Used to build
paulson@7290
    36
the image HOL-Real.
paulson@7290
    37
clasohm@1339
    38
<DT>Subst
paulson@7290
    39
<DD>defines a theory of substitution and unification.
paulson@7290
    40
paulson@7290
    41
<DT>Tools
paulson@7290
    42
<DD>holds code used to provide support for records, datatypes, induction, etc.
paulson@7290
    43
paulson@7290
    44
<DT>UNITY
paulson@7290
    45
<DD>Chandy and Misra's UNITY formalism.
clasohm@1339
    46
</DL>
clasohm@1339
    47
clasohm@1339
    48
Useful references on Higher-Order Logic:
clasohm@1339
    49
clasohm@1339
    50
<UL>
wenzelm@4622
    51
wenzelm@4622
    52
<LI> P. B. Andrews,<BR>
clasohm@1341
    53
    An Introduction to Mathematical Logic and Type Theory<BR>
clasohm@1341
    54
    (Academic Press, 1986).
clasohm@1339
    55
wenzelm@4622
    56
<P>
wenzelm@4622
    57
wenzelm@4622
    58
<LI> A. Church,<BR>
wenzelm@4622
    59
    A Formulation of the Simple Theory of Types<BR>
wenzelm@4622
    60
    (Journal of Symbolic Logic, 1940).
wenzelm@4622
    61
wenzelm@4622
    62
<P>
wenzelm@4622
    63
wenzelm@4622
    64
<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
wenzelm@4622
    65
    Introduction to HOL: A theorem proving environment for higher order logic<BR>
wenzelm@4622
    66
    (Cambridge University Press, 1993).
wenzelm@4622
    67
wenzelm@4622
    68
<P>
wenzelm@4622
    69
wenzelm@4622
    70
<LI> J. Lambek and P. J. Scott,<BR>
wenzelm@4622
    71
    Introduction to Higher Order Categorical Logic<BR>
wenzelm@4622
    72
    (Cambridge University Press, 1986).
wenzelm@4622
    73
clasohm@1339
    74
</UL>
clasohm@1339
    75
clasohm@1339
    76
</BODY></HTML>