src/HOL/README.html
author webertj
Sun Nov 14 01:40:27 2004 +0100 (2004-11-14)
changeset 15283 f21466450330
parent 14543 0e266a5dd6e3
child 15582 7219facb3fd0
permissions -rw-r--r--
DOCTYPE declaration added
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
wenzelm@10163
     3
<html>
wenzelm@10163
     4
paulson@2080
     5
<!-- $Id$ -->
clasohm@1339
     6
wenzelm@10163
     7
<head><title>HOL/README</title></head>
clasohm@1339
     8
wenzelm@10163
     9
<body>
wenzelm@10163
    10
wenzelm@10163
    11
<h2>HOL: Higher-Order Logic</h2>
clasohm@1339
    12
wenzelm@10262
    13
These are the main sources of the Isabelle system for Higher-Order Logic.
wenzelm@10163
    14
wenzelm@10163
    15
<p>
paulson@2080
    16
wenzelm@10163
    17
There are also several example sessions:
wenzelm@10163
    18
<dl>
paulson@2080
    19
wenzelm@10163
    20
<dt>Algebra
wenzelm@10163
    21
<dd>rings and univariate polynomials
wenzelm@10163
    22
wenzelm@10163
    23
<dt>Auth
wenzelm@10163
    24
<dd>a new approach to verifying authentication protocols
wenzelm@7303
    25
wenzelm@10163
    26
<dt>AxClasses
wenzelm@10163
    27
<dd>a few basic examples of using axiomatic type classes
wenzelm@10163
    28
wenzelm@10163
    29
<dt>BCV
wenzelm@10163
    30
<dd>generic model of bytecode verification, i.e. data-flow analysis
wenzelm@10163
    31
for assembly languages with subtypes
wenzelm@7303
    32
kleing@14024
    33
<dt>HOL-Complex
kleing@14024
    34
<dd>a development of the complex numbers, the reals, and the hyper-reals,
kleing@14024
    35
which are used in non-standard analysis (builds the image HOL-Complex)
wenzelm@7303
    36
kleing@14024
    37
<dt>HOL-Complex-HahnBanach
wenzelm@10163
    38
<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
wenzelm@7303
    39
kleing@14024
    40
<dt>HOL-Complex-ex
kleing@14024
    41
<dd>miscellaneous real ans complex number examples
wenzelm@10163
    42
wenzelm@10163
    43
<dt>Hoare
wenzelm@10163
    44
<dd>verification of imperative programs (verification conditions are
wenzelm@10163
    45
generated automatically from pre/post conditions and loop invariants)
wenzelm@7691
    46
wenzelm@10163
    47
<dt>IMP
wenzelm@10163
    48
<dd>mechanization of a large part of a semantics text by Glynn Winskel
nipkow@7291
    49
wenzelm@10163
    50
<dt>IMPP
wenzelm@10163
    51
<dd>extension of IMP with local variables and mutually recursive
wenzelm@10163
    52
procedures
paulson@2080
    53
wenzelm@10163
    54
<dt>IOA
wenzelm@10163
    55
<dd>a simple theory of Input/Output Automata
wenzelm@10163
    56
wenzelm@10163
    57
<dt>Induct
wenzelm@10163
    58
<dd>examples of (co)inductive definitions
paulson@3125
    59
wenzelm@10163
    60
<dt>Isar_examples
wenzelm@10163
    61
<dd>several introductory examples using Isabelle/Isar
paulson@2080
    62
wenzelm@10163
    63
<dt>Lambda
wenzelm@10163
    64
<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
paulson@2080
    65
wenzelm@10163
    66
<dt>Lattice
wenzelm@10163
    67
<dd>lattices and order structures (in Isabelle/Isar)
wenzelm@7303
    68
wenzelm@10163
    69
<dt>MicroJava
wenzelm@10163
    70
<dd>formalization of a fragment of Java, together with a corresponding
wenzelm@10163
    71
virtual machine and a specification of its bytecode verifier and a
wenzelm@10163
    72
lightweight bytecode verifier, including proofs of type-safety.
nipkow@7291
    73
wenzelm@10163
    74
<dt>Modelcheck
wenzelm@10163
    75
<dd>basic setup for integration of some model checkers in Isabelle/HOL
paulson@7290
    76
wenzelm@10163
    77
<dt>NumberTheory
wenzelm@10163
    78
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
wenzelm@10163
    79
Fermat/Euler Theorem, Wilson's Theorem
wenzelm@7662
    80
wenzelm@10163
    81
<dt>Prolog
wenzelm@10163
    82
<dd>a (bare-bones) implementation of Lambda-Prolog
wenzelm@10163
    83
wenzelm@10163
    84
<dt>Subst
wenzelm@10163
    85
<dd>defines a theory of substitution and unification.
paulson@7290
    86
wenzelm@10163
    87
<dt>TLA
wenzelm@10163
    88
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
nipkow@7291
    89
wenzelm@10163
    90
<dt>UNITY
wenzelm@10163
    91
<dd>Chandy and Misra's UNITY formalism
paulson@7290
    92
wenzelm@10163
    93
<dt>W0
wenzelm@10163
    94
<dd>a precursor of MiniML, without let-expressions
nipkow@7291
    95
wenzelm@10163
    96
<dt>ex
wenzelm@10163
    97
<dd>miscellaneous examples
wenzelm@10163
    98
wenzelm@10163
    99
</dl>
clasohm@1339
   100
clasohm@1339
   101
Useful references on Higher-Order Logic:
clasohm@1339
   102
wenzelm@10163
   103
<ul>
clasohm@1339
   104
wenzelm@10163
   105
<li>P. B. Andrews,<br>
wenzelm@10163
   106
An Introduction to Mathematical Logic and Type Theory<br>
wenzelm@10163
   107
(Academic Press, 1986).
wenzelm@4622
   108
wenzelm@10163
   109
<li>A. Church,<br>
wenzelm@10163
   110
A Formulation of the Simple Theory of Types<br>
wenzelm@10163
   111
(Journal of Symbolic Logic, 1940).
wenzelm@4622
   112
wenzelm@10163
   113
<li>M. J. C. Gordon and T. F. Melham (editors),<br>
wenzelm@10163
   114
Introduction to HOL: A theorem proving environment for higher order logic<br>
wenzelm@10163
   115
(Cambridge University Press, 1993).
wenzelm@4622
   116
wenzelm@10163
   117
<li>J. Lambek and P. J. Scott,<br>
wenzelm@10163
   118
Introduction to Higher Order Categorical Logic<br>
wenzelm@10163
   119
(Cambridge University Press, 1986).
wenzelm@4622
   120
wenzelm@10163
   121
</ul>
clasohm@1339
   122
wenzelm@10163
   123
</body>
wenzelm@10163
   124
</html>