author | wenzelm |
Thu, 07 Sep 2000 20:47:54 +0200 | |
changeset 9886 | 897d6602cbfb |
parent 9811 | 39ffdb8cab03 |
child 10163 | d1972b445ece |
permissions | -rw-r--r-- |
2080 | 1 |
<!-- $Id$ --> |
3279 | 2 |
<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY> |
1339 | 3 |
|
3279 | 4 |
<H2>HOL: Higher-Order Logic</H2> |
1339 | 5 |
|
3279 | 6 |
This directory contains the ML sources of the Isabelle system for |
7 |
Higher-Order Logic.<P> |
|
1339 | 8 |
|
3279 | 9 |
There are several subdirectories with examples: |
2080 | 10 |
<DL> |
1339 | 11 |
<DT>ex |
2080 | 12 |
<DD>general examples |
13 |
||
14 |
<DT>Auth |
|
15 |
<DD>a new approach to verifying authentication protocols |
|
16 |
||
7303 | 17 |
<DT>AxClasses |
18 |
<DD>a few axiomatic type class examples: |
|
19 |
<DL> |
|
20 |
||
21 |
<DT> Tutorial <DD> Some simple axclass demos that go along with the |
|
22 |
<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>). |
|
23 |
||
24 |
<DT> Group |
|
25 |
<DD> Some bits of group theory. |
|
26 |
||
27 |
<DT> Lattice |
|
28 |
<DD> Basic theory of lattices and orders. |
|
29 |
||
30 |
</DL> |
|
31 |
||
7691 | 32 |
<DT>BCV |
33 |
<DD>generic model of bytecode verification, i.e. data-flow analysis |
|
34 |
for assembly languages with subtypes. |
|
35 |
||
7291 | 36 |
<DT>Hoare |
37 |
<DD>verification of imperative programs; verification conditions are |
|
38 |
generated automatically from pre/post conditions and loop invariants. |
|
39 |
||
2080 | 40 |
<DT>IMP |
41 |
<DD>mechanization of a large part of a semantics text by Glynn Winskel |
|
42 |
||
3125 | 43 |
<DT>Induct |
44 |
<DD>examples of (co)inductive definitions |
|
45 |
||
7290 | 46 |
<DT>Integ |
47 |
<DD>a development of the integers including efficient integer |
|
48 |
calculations (part of the standard HOL environment) |
|
2080 | 49 |
|
50 |
<DT>IOA |
|
7291 | 51 |
<DD>a simple theory of Input/Output Automata |
2080 | 52 |
|
7303 | 53 |
<DT>Isar_examples |
7983 | 54 |
<DD>several introductory Isabelle/Isar examples |
7303 | 55 |
|
2080 | 56 |
<DT>Lambda |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
7983
diff
changeset
|
57 |
<DD>fundamental properties of lambda-calculus (Church-Rosser and termination) |
1339 | 58 |
|
7291 | 59 |
<DT>Lex |
60 |
<DD>verification of a simple lexical analyzer generator |
|
61 |
||
62 |
<DT>MiniML |
|
63 |
<DD>formalization of type inference for the language Mini-ML |
|
64 |
||
7290 | 65 |
<DT>Real |
66 |
<DD>a development of the reals and hyper-reals, which are used in |
|
67 |
non-standard analysis. Also includes the positive rationals. Used to build |
|
68 |
the image HOL-Real. |
|
69 |
||
7662 | 70 |
<DT>Real/HahnBanach |
71 |
<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar). |
|
72 |
||
1339 | 73 |
<DT>Subst |
7290 | 74 |
<DD>defines a theory of substitution and unification. |
75 |
||
7291 | 76 |
<DT>TLA |
77 |
<DD>Lamport's Temporal Logic of Actions |
|
78 |
||
7290 | 79 |
<DT>Tools |
80 |
<DD>holds code used to provide support for records, datatypes, induction, etc. |
|
81 |
||
82 |
<DT>UNITY |
|
83 |
<DD>Chandy and Misra's UNITY formalism. |
|
7291 | 84 |
|
85 |
<DT>W0 |
|
86 |
<DD>a precursor of MiniML, without let-expressions |
|
1339 | 87 |
</DL> |
88 |
||
89 |
Useful references on Higher-Order Logic: |
|
90 |
||
91 |
<UL> |
|
4622 | 92 |
|
93 |
<LI> P. B. Andrews,<BR> |
|
1341 | 94 |
An Introduction to Mathematical Logic and Type Theory<BR> |
95 |
(Academic Press, 1986). |
|
1339 | 96 |
|
4622 | 97 |
<P> |
98 |
||
99 |
<LI> A. Church,<BR> |
|
100 |
A Formulation of the Simple Theory of Types<BR> |
|
101 |
(Journal of Symbolic Logic, 1940). |
|
102 |
||
103 |
<P> |
|
104 |
||
105 |
<LI> M. J. C. Gordon and T. F. Melham (editors),<BR> |
|
106 |
Introduction to HOL: A theorem proving environment for higher order logic<BR> |
|
107 |
(Cambridge University Press, 1993). |
|
108 |
||
109 |
<P> |
|
110 |
||
111 |
<LI> J. Lambek and P. J. Scott,<BR> |
|
112 |
Introduction to Higher Order Categorical Logic<BR> |
|
113 |
(Cambridge University Press, 1986). |
|
114 |
||
1339 | 115 |
</UL> |
116 |
||
117 |
</BODY></HTML> |