src/HOL/README.html
author paulson
Mon, 02 Aug 1999 11:24:30 +0200
changeset 7143 9c02848c5404
parent 4622 85aae356570c
child 7290 f1a37c379317
permissions -rw-r--r--
the SVC link-up

<!-- $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>