<!-- $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).
<LI>J. Lambek and P. J. Scott,<BR>
Introduction to Higher Order Categorical Logic (CUP, 1986)
</UL>
</BODY></HTML>