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