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