<!-- $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>AxClasses
<DD>a few axiomatic type class examples:
<DL>
<DT> Tutorial <DD> Some simple axclass demos that go along with the
<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
<DT> Group
<DD> Some bits of group theory.
<DT> Lattice
<DD> Basic theory of lattices and orders.
</DL>
<DT>BCV
<DD>generic model of bytecode verification, i.e. data-flow analysis
for assembly languages with subtypes.
<DT>Hoare
<DD>verification of imperative programs; verification conditions are
generated automatically from pre/post conditions and loop invariants.
<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 development of the integers including efficient integer
calculations (part of the standard HOL environment)
<DT>IOA
<DD>a simple theory of Input/Output Automata
<DT>Isar_examples
<DD>several introductory Isabelle/Isar examples
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus
<DT>Lex
<DD>verification of a simple lexical analyzer generator
<DT>MiniML
<DD>formalization of type inference for the language Mini-ML
<DT>Real
<DD>a development of the reals and hyper-reals, which are used in
non-standard analysis. Also includes the positive rationals. Used to build
the image HOL-Real.
<DT>Real/HahnBanach
<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
<DT>Subst
<DD>defines a theory of substitution and unification.
<DT>TLA
<DD>Lamport's Temporal Logic of Actions
<DT>Tools
<DD>holds code used to provide support for records, datatypes, induction, etc.
<DT>UNITY
<DD>Chandy and Misra's UNITY formalism.
<DT>W0
<DD>a precursor of MiniML, without let-expressions
</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>