author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 33028 | 9aa8bfb1649d |
child 36862 | 952b2b102a0a |
permissions | -rw-r--r-- |
15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
15582 | 3 |
<!-- $Id$ --> |
4 |
||
10163 | 5 |
<html> |
6 |
||
15582 | 7 |
<head> |
8 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
9 |
<title>HOL/README</title> |
|
10 |
</head> |
|
1339 | 11 |
|
10163 | 12 |
<body> |
13 |
||
14 |
<h2>HOL: Higher-Order Logic</h2> |
|
1339 | 15 |
|
10262 | 16 |
These are the main sources of the Isabelle system for Higher-Order Logic. |
10163 | 17 |
|
18 |
<p> |
|
2080 | 19 |
|
10163 | 20 |
There are also several example sessions: |
21 |
<dl> |
|
2080 | 22 |
|
10163 | 23 |
<dt>Algebra |
24 |
<dd>rings and univariate polynomials |
|
25 |
||
26 |
<dt>Auth |
|
27 |
<dd>a new approach to verifying authentication protocols |
|
7303 | 28 |
|
10163 | 29 |
<dt>AxClasses |
30 |
<dd>a few basic examples of using axiomatic type classes |
|
31 |
||
15910 | 32 |
<dt>Complex |
14024 | 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) |
|
7303 | 35 |
|
10163 | 36 |
<dt>Hoare |
37 |
<dd>verification of imperative programs (verification conditions are |
|
38 |
generated automatically from pre/post conditions and loop invariants) |
|
7691 | 39 |
|
15910 | 40 |
<dt>HoareParallel |
41 |
<dd>verification of shared-variable imperative programs a la Owicki-Gries. |
|
42 |
(verification conditions are generated automatically) |
|
43 |
||
44 |
<dt>Hyperreal |
|
45 |
<dd>Nonstandard analysis. Builds on Real and is part of Complex. |
|
46 |
||
10163 | 47 |
<dt>IMP |
48 |
<dd>mechanization of a large part of a semantics text by Glynn Winskel |
|
7291 | 49 |
|
10163 | 50 |
<dt>IMPP |
51 |
<dd>extension of IMP with local variables and mutually recursive |
|
52 |
procedures |
|
2080 | 53 |
|
15910 | 54 |
<dt>Import |
55 |
<dd>theories imported from other (HOL) theorem provers. |
|
10163 | 56 |
|
57 |
<dt>Induct |
|
58 |
<dd>examples of (co)inductive definitions |
|
3125 | 59 |
|
15910 | 60 |
<dt>IOA |
61 |
<dd>a simple theory of Input/Output Automata |
|
62 |
||
33026 | 63 |
<dt>Isar_Examples |
10163 | 64 |
<dd>several introductory examples using Isabelle/Isar |
2080 | 65 |
|
10163 | 66 |
<dt>Lambda |
67 |
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination) |
|
2080 | 68 |
|
10163 | 69 |
<dt>Lattice |
70 |
<dd>lattices and order structures (in Isabelle/Isar) |
|
7303 | 71 |
|
15910 | 72 |
<dt>Library |
73 |
<dd>A collection of generic theories |
|
74 |
||
75 |
<dt>Matrix |
|
76 |
<dd>two-dimensional matrices |
|
77 |
||
10163 | 78 |
<dt>MicroJava |
79 |
<dd>formalization of a fragment of Java, together with a corresponding |
|
80 |
virtual machine and a specification of its bytecode verifier and a |
|
15910 | 81 |
lightweight bytecode verifier, including proofs of type-safety |
7291 | 82 |
|
10163 | 83 |
<dt>Modelcheck |
84 |
<dd>basic setup for integration of some model checkers in Isabelle/HOL |
|
7290 | 85 |
|
15910 | 86 |
<dt>NanoJava |
87 |
<dd>Haore Logic for a tiny fragment of Java |
|
88 |
||
10163 | 89 |
<dt>NumberTheory |
90 |
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
|
15910 | 91 |
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity |
7662 | 92 |
|
10163 | 93 |
<dt>Prolog |
94 |
<dd>a (bare-bones) implementation of Lambda-Prolog |
|
95 |
||
15910 | 96 |
<dt>Real |
97 |
<dd>the real numbers, part of Complex |
|
98 |
||
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
15916
diff
changeset
|
99 |
<dt>Hahn_Banach |
15910 | 100 |
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) |
101 |
||
33028 | 102 |
<dt>SET_Protocol |
15910 | 103 |
<dd>verification of the SET Protocol |
104 |
||
10163 | 105 |
<dt>Subst |
15910 | 106 |
<dd>a theory of substitution and unification. |
7290 | 107 |
|
10163 | 108 |
<dt>TLA |
109 |
<dd>Lamport's Temporal Logic of Actions (with separate example sessions) |
|
7291 | 110 |
|
10163 | 111 |
<dt>UNITY |
112 |
<dd>Chandy and Misra's UNITY formalism |
|
7290 | 113 |
|
10163 | 114 |
<dt>W0 |
115 |
<dd>a precursor of MiniML, without let-expressions |
|
7291 | 116 |
|
10163 | 117 |
<dt>ex |
118 |
<dd>miscellaneous examples |
|
119 |
||
120 |
</dl> |
|
1339 | 121 |
|
10163 | 122 |
</body> |
123 |
</html> |