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