src/HOL/README.html
author ballarin
Thu, 11 Dec 2008 18:30:26 +0100
changeset 29223 e09c53289830
parent 15916 1314ef1e49dd
child 31795 be3e1cc5005c
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 14543
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 14543
diff changeset
     2
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     3
<!-- $Id$ -->
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     4
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     5
<html>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     6
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
<head>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     9
  <title>HOL/README</title>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
    10
</head>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    11
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    12
<body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    13
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    14
<h2>HOL: Higher-Order Logic</h2>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    15
10262
wenzelm
parents: 10163
diff changeset
    16
These are the main sources of the Isabelle system for Higher-Order Logic.
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    17
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    18
<p>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    19
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    20
There are also several example sessions:
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    21
<dl>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    22
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    23
<dt>Algebra
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    24
<dd>rings and univariate polynomials
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    25
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    26
<dt>Auth
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    27
<dd>a new approach to verifying authentication protocols
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    28
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    29
<dt>AxClasses
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    30
<dd>a few basic examples of using axiomatic type classes
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    31
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    32
<dt>Complex
14024
213dcc39358f HOL-Real -> HOL-Complex
kleing
parents: 13852
diff changeset
    33
<dd>a development of the complex numbers, the reals, and the hyper-reals,
213dcc39358f HOL-Real -> HOL-Complex
kleing
parents: 13852
diff changeset
    34
which are used in non-standard analysis (builds the image HOL-Complex)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    35
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    36
<dt>Hoare
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    37
<dd>verification of imperative programs (verification conditions are
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    38
generated automatically from pre/post conditions and loop invariants)
7691
b7e8277fa088 added BVC;
wenzelm
parents: 7662
diff changeset
    39
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    40
<dt>HoareParallel
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    41
<dd>verification of shared-variable imperative programs a la Owicki-Gries.
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    42
(verification conditions are generated automatically)
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    43
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    44
<dt>Hyperreal
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    45
<dd>Nonstandard analysis. Builds on Real and is part of Complex.
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    46
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    47
<dt>IMP
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    48
<dd>mechanization of a large part of a semantics text by Glynn Winskel
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    49
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    50
<dt>IMPP
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    51
<dd>extension of IMP with local variables and mutually recursive
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    52
procedures
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    53
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    54
<dt>Import
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    55
<dd>theories imported from other (HOL) theorem provers.
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    56
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    57
<dt>Induct
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    58
<dd>examples of (co)inductive definitions
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 2080
diff changeset
    59
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    60
<dt>IOA
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    61
<dd>a simple theory of Input/Output Automata
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    62
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    63
<dt>Isar_examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    64
<dd>several introductory examples using Isabelle/Isar
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    65
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    66
<dt>Lambda
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    67
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    68
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    69
<dt>Lattice
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    70
<dd>lattices and order structures (in Isabelle/Isar)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    71
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    72
<dt>Library
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    73
<dd>A collection of generic theories
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    74
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    75
<dt>Matrix
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    76
<dd>two-dimensional matrices
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    77
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    78
<dt>MicroJava
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    79
<dd>formalization of a fragment of Java, together with a corresponding
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    80
virtual machine and a specification of its bytecode verifier and a
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    81
lightweight bytecode verifier, including proofs of type-safety
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    82
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    83
<dt>Modelcheck
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    84
<dd>basic setup for integration of some model checkers in Isabelle/HOL
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
    85
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    86
<dt>NanoJava
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    87
<dd>Haore Logic for a tiny fragment of Java
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    88
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    89
<dt>NumberTheory
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    90
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    91
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
7662
062a782d7402 Real/HahnBanach;
wenzelm
parents: 7303
diff changeset
    92
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    93
<dt>Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    94
<dd>a (bare-bones) implementation of Lambda-Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    95
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    96
<dt>Real
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    97
<dd>the real numbers, part of Complex
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    98
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    99
<dt>Real/HahnBanach
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   100
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   101
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   102
<dt>SET-Protocol
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   103
<dd>verification of the SET Protocol
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   104
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   105
<dt>Subst
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   106
<dd>a theory of substitution and unification.
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
   107
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   108
<dt>TLA
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   109
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
   110
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   111
<dt>UNITY
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   112
<dd>Chandy and Misra's UNITY formalism
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
   113
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   114
<dt>W0
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   115
<dd>a precursor of MiniML, without let-expressions
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
   116
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   117
<dt>ex
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   118
<dd>miscellaneous examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   119
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   120
</dl>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   121
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   122
</body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   123
</html>