src/HOL/README.html
author wenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279 815ef5848324
parent 3125 3f0ab2c306f7
child 4622 85aae356570c
permissions -rw-r--r--
tuned all READMEs;
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@2080
    23
<DT>Integ
paulson@2080
    24
<DD>a theory of the integers including efficient integer calculations
paulson@2080
    25
paulson@2080
    26
<DT>IOA
paulson@3125
    27
<DD>extended example of Input/Output Automata
paulson@2080
    28
paulson@2080
    29
<DT>Lambda
paulson@2080
    30
<DD>a proof of the Church-Rosser theorem for lambda-calculus
clasohm@1339
    31
clasohm@1339
    32
<DT>Subst
clasohm@1339
    33
<DD>subdirectory defining a theory of substitution and unification.
clasohm@1339
    34
</DL>
clasohm@1339
    35
clasohm@1339
    36
Useful references on Higher-Order Logic:
clasohm@1339
    37
clasohm@1339
    38
<UL>
clasohm@1341
    39
<LI>P. B. Andrews,<BR>
clasohm@1341
    40
    An Introduction to Mathematical Logic and Type Theory<BR>
clasohm@1341
    41
    (Academic Press, 1986).
clasohm@1339
    42
clasohm@1341
    43
<LI>J. Lambek and P. J. Scott,<BR>
clasohm@1341
    44
    Introduction to Higher Order Categorical Logic (CUP, 1986)
clasohm@1339
    45
</UL>
clasohm@1339
    46
clasohm@1339
    47
</BODY></HTML>