src/HOL/README.html
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 36862 952b2b102a0a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     3
<html>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
     4
15582
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     5
<head>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     7
  <title>HOL/README</title>
7219facb3fd0 HTML 4.01 Transitional conformity
webertj
parents: 15283
diff changeset
     8
</head>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     9
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    10
<body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    11
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    12
<h2>HOL: Higher-Order Logic</h2>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    13
10262
wenzelm
parents: 10163
diff changeset
    14
These are the main sources of the Isabelle system for Higher-Order Logic.
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    15
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    16
<p>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    17
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    18
There are also several example sessions:
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    19
<dl>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    20
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    21
<dt>Algebra
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    22
<dd>rings and univariate polynomials
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    23
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    24
<dt>Auth
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    25
<dd>a new approach to verifying authentication protocols
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    26
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    27
<dt>AxClasses
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    28
<dd>a few basic examples of using axiomatic type classes
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    29
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    30
<dt>Complex
14024
213dcc39358f HOL-Real -> HOL-Complex
kleing
parents: 13852
diff changeset
    31
<dd>a development of the complex numbers, the reals, and the hyper-reals,
213dcc39358f HOL-Real -> HOL-Complex
kleing
parents: 13852
diff changeset
    32
which are used in non-standard analysis (builds the image HOL-Complex)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    33
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    34
<dt>Hoare
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    35
<dd>verification of imperative programs (verification conditions are
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    36
generated automatically from pre/post conditions and loop invariants)
7691
b7e8277fa088 added BVC;
wenzelm
parents: 7662
diff changeset
    37
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    38
<dt>HoareParallel
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    39
<dd>verification of shared-variable imperative programs a la Owicki-Gries.
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    40
(verification conditions are generated automatically)
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    41
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    42
<dt>Hyperreal
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    43
<dd>Nonstandard analysis. Builds on Real and is part of Complex.
5df57194d064 *** empty log message ***
nipkow
parents: 15582
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
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    52
<dt>Import
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    53
<dd>theories imported from other (HOL) theorem provers.
10163
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
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    58
<dt>IOA
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    59
<dd>a simple theory of Input/Output Automata
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    60
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 31795
diff changeset
    61
<dt>Isar_Examples
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    62
<dd>several introductory examples using Isabelle/Isar
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    63
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    64
<dt>Lambda
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    65
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    66
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    67
<dt>Lattice
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    68
<dd>lattices and order structures (in Isabelle/Isar)
7303
96bc013c8987 AxClasses, Isar_examples;
wenzelm
parents: 7291
diff changeset
    69
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    70
<dt>Library
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    71
<dd>A collection of generic theories
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    72
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    73
<dt>Matrix
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    74
<dd>two-dimensional matrices
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    75
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    76
<dt>MicroJava
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    77
<dd>formalization of a fragment of Java, together with a corresponding
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    78
virtual machine and a specification of its bytecode verifier and a
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    79
lightweight bytecode verifier, including proofs of type-safety
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
    80
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    81
<dt>Modelcheck
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    82
<dd>basic setup for integration of some model checkers in Isabelle/HOL
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
    83
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    84
<dt>NanoJava
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    85
<dd>Haore Logic for a tiny fragment of Java
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    86
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    87
<dt>NumberTheory
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    88
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    89
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
7662
062a782d7402 Real/HahnBanach;
wenzelm
parents: 7303
diff changeset
    90
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    91
<dt>Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    92
<dd>a (bare-bones) implementation of Lambda-Prolog
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
    93
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    94
<dt>Real
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    95
<dd>the real numbers, part of Complex
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    96
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 15916
diff changeset
    97
<dt>Hahn_Banach
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    98
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
    99
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33026
diff changeset
   100
<dt>SET_Protocol
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   101
<dd>verification of the SET Protocol
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   102
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   103
<dt>Subst
15910
5df57194d064 *** empty log message ***
nipkow
parents: 15582
diff changeset
   104
<dd>a theory of substitution and unification.
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
   105
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   106
<dt>TLA
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   107
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
   108
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   109
<dt>UNITY
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   110
<dd>Chandy and Misra's UNITY formalism
7290
f1a37c379317 updated
paulson
parents: 4622
diff changeset
   111
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   112
<dt>W0
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   113
<dd>a precursor of MiniML, without let-expressions
7291
8aa66ddc0bea new entriues.
nipkow
parents: 7290
diff changeset
   114
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   115
<dt>ex
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   116
<dd>miscellaneous examples
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   117
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   118
</dl>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
   119
10163
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   120
</body>
d1972b445ece updated, improved;
wenzelm
parents: 9811
diff changeset
   121
</html>