<!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 aregenerated 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 recursiveprocedures<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 correspondingvirtual machine and a specification of its bytecode verifier and alightweight 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>