src/HOL/README.html
author wenzelm
Tue, 24 Nov 1998 12:03:09 +0100
changeset 5953 d6017ce6b93e
parent 4622 85aae356570c
child 7290 f1a37c379317
permissions -rw-r--r--
setup Blast.setup; setup Clasimp.setup;

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>

<H2>HOL: Higher-Order Logic</H2>

This directory contains the ML sources of the Isabelle system for
Higher-Order Logic.<P>

There are several subdirectories with examples:
<DL>
<DT>ex
<DD>general examples

<DT>Auth
<DD>a new approach to verifying authentication protocols 

<DT>IMP
<DD>mechanization of a large part of a semantics text by Glynn Winskel

<DT>Induct
<DD>examples of (co)inductive definitions

<DT>Integ
<DD>a theory of the integers including efficient integer calculations

<DT>IOA
<DD>extended example of Input/Output Automata

<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus

<DT>Subst
<DD>subdirectory defining a theory of substitution and unification.
</DL>

Useful references on Higher-Order Logic:

<UL>

<LI> P. B. Andrews,<BR>
    An Introduction to Mathematical Logic and Type Theory<BR>
    (Academic Press, 1986).

<P>

<LI> A. Church,<BR>
    A Formulation of the Simple Theory of Types<BR>
    (Journal of Symbolic Logic, 1940).

<P>

<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
    Introduction to HOL: A theorem proving environment for higher order logic<BR>
    (Cambridge University Press, 1993).

<P>

<LI> J. Lambek and P. J. Scott,<BR>
    Introduction to Higher Order Categorical Logic<BR>
    (Cambridge University Press, 1986).

</UL>

</BODY></HTML>