<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<title>HOL/README</title>
</head>
<body>
<h2>HOL: Higher-Order Logic</h2>
These are the main sources of the Isabelle system for Higher-Order Logic.
<p>
There are also several example sessions:
<dl>
<dt>Algebra
<dd>rings and univariate polynomials
<dt>Auth
<dd>a new approach to verifying authentication protocols
<dt>AxClasses
<dd>a few basic examples of using axiomatic type classes
<dt>Complex
<dd>a development of the complex numbers, the reals, and the hyper-reals,
which are used in non-standard analysis (builds the image HOL-Complex)
<dt>Hoare
<dd>verification of imperative programs (verification conditions are
generated automatically from pre/post conditions and loop invariants)
<dt>HoareParallel
<dd>verification of shared-variable imperative programs a la Owicki-Gries.
(verification conditions are generated automatically)
<dt>Hyperreal
<dd>Nonstandard analysis. Builds on Real and is part of Complex.
<dt>IMP
<dd>mechanization of a large part of a semantics text by Glynn Winskel
<dt>IMPP
<dd>extension of IMP with local variables and mutually recursive
procedures
<dt>Import
<dd>theories imported from other (HOL) theorem provers.
<dt>Induct
<dd>examples of (co)inductive definitions
<dt>IOA
<dd>a simple theory of Input/Output Automata
<dt>Isar_examples
<dd>several introductory examples using Isabelle/Isar
<dt>Lambda
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
<dt>Lattice
<dd>lattices and order structures (in Isabelle/Isar)
<dt>Library
<dd>A collection of generic theories
<dt>Matrix
<dd>two-dimensional matrices
<dt>MicroJava
<dd>formalization of a fragment of Java, together with a corresponding
virtual machine and a specification of its bytecode verifier and a
lightweight bytecode verifier, including proofs of type-safety
<dt>Modelcheck
<dd>basic setup for integration of some model checkers in Isabelle/HOL
<dt>NanoJava
<dd>Haore Logic for a tiny fragment of Java
<dt>NumberTheory
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
<dt>Prolog
<dd>a (bare-bones) implementation of Lambda-Prolog
<dt>Real
<dd>the real numbers, part of Complex
<dt>Hahn_Banach
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
<dt>SET-Protocol
<dd>verification of the SET Protocol
<dt>Subst
<dd>a theory of substitution and unification.
<dt>TLA
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
<dt>UNITY
<dd>Chandy and Misra's UNITY formalism
<dt>W0
<dd>a precursor of MiniML, without let-expressions
<dt>ex
<dd>miscellaneous examples
</dl>
</body>
</html>