src/HOL/README.html
author wenzelm
Wed, 18 Oct 2000 23:40:38 +0200
changeset 10262 3c43e8086cba
parent 10163 d1972b445ece
child 13852 dd2cd94a51e6
permissions -rw-r--r--
tuned;

<html>

<!-- $Id$ -->

<head><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>BCV
<dd>generic model of bytecode verification, i.e. data-flow analysis
for assembly languages with subtypes

<dt>HOL-Real
<dd>a development of the reals and hyper-reals, which are used in
non-standard analysis (builds the image HOL-Real)

<dt>HOL-Real-HahnBanach
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)

<dt>HOL-Real-ex
<dd>miscellaneous real number examples

<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>IMPP
<dd>extension of IMP with local variables and mutually recursive
procedures

<dt>IOA
<dd>a simple theory of Input/Output Automata

<dt>Induct
<dd>examples of (co)inductive definitions

<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>Lex
<dd>verification of a simple lexical analyzer generator

<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>MiniML
<dd>formalization of type inference for the language Mini-ML

<dt>Modelcheck
<dd>basic setup for integration of some model checkers in Isabelle/HOL

<dt>NumberTheory
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
Fermat/Euler Theorem, Wilson's Theorem

<dt>Prolog
<dd>a (bare-bones) implementation of Lambda-Prolog

<dt>Subst
<dd>defines 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>

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>A. Church,<br>
A Formulation of the Simple Theory of Types<br>
(Journal of Symbolic Logic, 1940).

<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).

<li>J. Lambek and P. J. Scott,<br>
Introduction to Higher Order Categorical Logic<br>
(Cambridge University Press, 1986).

</ul>

</body>
</html>