1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
8 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
9 <title>HOL/README</title>
14 <h2>HOL: Higher-Order Logic</h2>
16 These are the main sources of the Isabelle system for Higher-Order Logic.
20 There are also several example sessions:
24 <dd>rings and univariate polynomials
27 <dd>a new approach to verifying authentication protocols
30 <dd>a few basic examples of using axiomatic type classes
33 <dd>a development of the complex numbers, the reals, and the hyper-reals,
34 which are used in non-standard analysis (builds the image HOL-Complex)
37 <dd>verification of imperative programs (verification conditions are
38 generated automatically from pre/post conditions and loop invariants)
41 <dd>verification of shared-variable imperative programs a la Owicki-Gries.
42 (verification conditions are generated automatically)
45 <dd>Nonstandard analysis. Builds on Real and is part of Complex.
48 <dd>mechanization of a large part of a semantics text by Glynn Winskel
51 <dd>extension of IMP with local variables and mutually recursive
55 <dd>theories imported from other (HOL) theorem provers.
58 <dd>examples of (co)inductive definitions
61 <dd>a simple theory of Input/Output Automata
64 <dd>several introductory examples using Isabelle/Isar
67 <dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
70 <dd>lattices and order structures (in Isabelle/Isar)
73 <dd>A collection of generic theories
76 <dd>two-dimensional matrices
79 <dd>formalization of a fragment of Java, together with a corresponding
80 virtual machine and a specification of its bytecode verifier and a
81 lightweight bytecode verifier, including proofs of type-safety
84 <dd>basic setup for integration of some model checkers in Isabelle/HOL
87 <dd>Haore Logic for a tiny fragment of Java
90 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
91 Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
94 <dd>a (bare-bones) implementation of Lambda-Prolog
97 <dd>the real numbers, part of Complex
100 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
103 <dd>verification of the SET Protocol
106 <dd>a theory of substitution and unification.
109 <dd>Lamport's Temporal Logic of Actions (with separate example sessions)
112 <dd>Chandy and Misra's UNITY formalism
115 <dd>a precursor of MiniML, without let-expressions
118 <dd>miscellaneous examples