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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     1
<html>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     2
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
     3
<!-- $Id$ -->
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     4
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     5
<head><title>HOL/README</title></head>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     6
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     7
<body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     8
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     9
<h2>HOL: Higher-Order Logic</h2>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    10
10262
wenzelm
parents: 10163
diff changeset
    11
These are the main sources of the Isabelle system for Higher-Order Logic.
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    12
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    13
<p>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    14
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    15
There are also several example sessions:
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    16
<dl>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    17
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    18
<dt>Algebra
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    19
<dd>rings and univariate polynomials
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    20
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    21
<dt>Auth
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    22
<dd>a new approach to verifying authentication protocols
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    23
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    24
<dt>AxClasses
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    25
<dd>a few basic examples of using axiomatic type classes
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    26
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    27
<dt>BCV
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    28
<dd>generic model of bytecode verification, i.e. data-flow analysis
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    29
for assembly languages with subtypes
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    30
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    31
<dt>HOL-Real
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    32
<dd>a development of the reals and hyper-reals, which are used in
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    33
non-standard analysis (builds the image HOL-Real)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    34
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    35
<dt>HOL-Real-HahnBanach
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    36
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    37
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    38
<dt>HOL-Real-ex
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    39
<dd>miscellaneous real number examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    40
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    41
<dt>Hoare
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    42
<dd>verification of imperative programs (verification conditions are
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    43
generated automatically from pre/post conditions and loop invariants)
7691
b7e8277fa088 added BVC;
wenzelm
parents: 7662
diff changeset
    44
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    45
<dt>IMP
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    46
<dd>mechanization of a large part of a semantics text by Glynn Winskel
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    47
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    48
<dt>IMPP
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    49
<dd>extension of IMP with local variables and mutually recursive
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    50
procedures
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    51
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    52
<dt>IOA
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    53
<dd>a simple theory of Input/Output Automata
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    54
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    55
<dt>Induct
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    56
<dd>examples of (co)inductive definitions
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 2080
diff changeset
    57
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    58
<dt>Isar_examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    59
<dd>several introductory examples using Isabelle/Isar
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    60
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    61
<dt>Lambda
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    62
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    63
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    64
<dt>Lattice
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    65
<dd>lattices and order structures (in Isabelle/Isar)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    66
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    67
<dt>Lex
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    68
<dd>verification of a simple lexical analyzer generator
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    69
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    70
<dt>MicroJava
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    71
<dd>formalization of a fragment of Java, together with a corresponding
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    72
virtual machine and a specification of its bytecode verifier and a
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    73
lightweight bytecode verifier, including proofs of type-safety.
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    74
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    75
<dt>MiniML
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    76
<dd>formalization of type inference for the language Mini-ML
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    77
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    78
<dt>Modelcheck
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    79
<dd>basic setup for integration of some model checkers in Isabelle/HOL
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
    80
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    81
<dt>NumberTheory
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    82
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    83
Fermat/Euler Theorem, Wilson's Theorem
7662
062a782d7402 Real/HahnBanach;
wenzelm
parents: 7303
diff changeset
    84
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    85
<dt>Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    86
<dd>a (bare-bones) implementation of Lambda-Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    87
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    88
<dt>Subst
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    89
<dd>defines a theory of substitution and unification.
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
    90
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    91
<dt>TLA
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    92
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    93
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    94
<dt>UNITY
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    95
<dd>Chandy and Misra's UNITY formalism
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
    96
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    97
<dt>W0
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    98
<dd>a precursor of MiniML, without let-expressions
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    99
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   100
<dt>ex
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   101
<dd>miscellaneous examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   102
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   103
</dl>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   104
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   105
Useful references on Higher-Order Logic:
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   106
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   107
<ul>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   108
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   109
<li>P. B. Andrews,<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   110
An Introduction to Mathematical Logic and Type Theory<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   111
(Academic Press, 1986).
4622
wenzelm
parents: 3279
diff changeset
   112
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   113
<li>A. Church,<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   114
A Formulation of the Simple Theory of Types<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   115
(Journal of Symbolic Logic, 1940).
4622
wenzelm
parents: 3279
diff changeset
   116
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   117
<li>M. J. C. Gordon and T. F. Melham (editors),<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   118
Introduction to HOL: A theorem proving environment for higher order logic<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   119
(Cambridge University Press, 1993).
4622
wenzelm
parents: 3279
diff changeset
   120
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   121
<li>J. Lambek and P. J. Scott,<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   122
Introduction to Higher Order Categorical Logic<br>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   123
(Cambridge University Press, 1986).
4622
wenzelm
parents: 3279
diff changeset
   124
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   125
</ul>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   126
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   127
</body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   128
</html>