src/HOL/README.html
author wenzelm
Sat Oct 30 20:21:46 1999 +0200 (1999-10-30)
changeset 7983 d823fdcc0645
parent 7691 b7e8277fa088
child 9811 39ffdb8cab03
permissions -rw-r--r--
tuned;
paulson@2080
     1
<!-- $Id$ -->
wenzelm@3279
     2
<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
clasohm@1339
     3
wenzelm@3279
     4
<H2>HOL: Higher-Order Logic</H2>
clasohm@1339
     5
wenzelm@3279
     6
This directory contains the ML sources of the Isabelle system for
wenzelm@3279
     7
Higher-Order Logic.<P>
clasohm@1339
     8
wenzelm@3279
     9
There are several subdirectories with examples:
paulson@2080
    10
<DL>
clasohm@1339
    11
<DT>ex
paulson@2080
    12
<DD>general examples
paulson@2080
    13
paulson@2080
    14
<DT>Auth
paulson@2080
    15
<DD>a new approach to verifying authentication protocols 
paulson@2080
    16
wenzelm@7303
    17
<DT>AxClasses
wenzelm@7303
    18
<DD>a few axiomatic type class examples:
wenzelm@7303
    19
<DL>
wenzelm@7303
    20
wenzelm@7303
    21
<DT> Tutorial <DD> Some simple axclass demos that go along with the
wenzelm@7303
    22
<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
wenzelm@7303
    23
wenzelm@7303
    24
<DT> Group
wenzelm@7303
    25
<DD> Some bits of group theory.
wenzelm@7303
    26
wenzelm@7303
    27
<DT> Lattice
wenzelm@7303
    28
<DD> Basic theory of lattices and orders.
wenzelm@7303
    29
wenzelm@7303
    30
</DL>
wenzelm@7303
    31
wenzelm@7691
    32
<DT>BCV
wenzelm@7691
    33
<DD>generic model of bytecode verification, i.e. data-flow analysis
wenzelm@7691
    34
for assembly languages with subtypes.
wenzelm@7691
    35
nipkow@7291
    36
<DT>Hoare
nipkow@7291
    37
<DD>verification of imperative programs; verification conditions are
nipkow@7291
    38
generated automatically from pre/post conditions and loop invariants.
nipkow@7291
    39
paulson@2080
    40
<DT>IMP
paulson@2080
    41
<DD>mechanization of a large part of a semantics text by Glynn Winskel
paulson@2080
    42
paulson@3125
    43
<DT>Induct
paulson@3125
    44
<DD>examples of (co)inductive definitions
paulson@3125
    45
paulson@7290
    46
<DT>Integ 
paulson@7290
    47
<DD>a development of the integers including efficient integer
paulson@7290
    48
calculations (part of the standard HOL environment)
paulson@2080
    49
paulson@2080
    50
<DT>IOA
nipkow@7291
    51
<DD>a simple theory of Input/Output Automata
paulson@2080
    52
wenzelm@7303
    53
<DT>Isar_examples
wenzelm@7983
    54
<DD>several introductory Isabelle/Isar examples
wenzelm@7303
    55
paulson@2080
    56
<DT>Lambda
paulson@2080
    57
<DD>a proof of the Church-Rosser theorem for lambda-calculus
clasohm@1339
    58
nipkow@7291
    59
<DT>Lex
nipkow@7291
    60
<DD>verification of a simple lexical analyzer generator
nipkow@7291
    61
nipkow@7291
    62
<DT>MiniML
nipkow@7291
    63
<DD>formalization of type inference for the language Mini-ML
nipkow@7291
    64
paulson@7290
    65
<DT>Real 
paulson@7290
    66
<DD>a development of the reals and hyper-reals, which are used in
paulson@7290
    67
non-standard analysis.  Also includes the positive rationals.  Used to build
paulson@7290
    68
the image HOL-Real.
paulson@7290
    69
wenzelm@7662
    70
<DT>Real/HahnBanach
wenzelm@7662
    71
<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
wenzelm@7662
    72
clasohm@1339
    73
<DT>Subst
paulson@7290
    74
<DD>defines a theory of substitution and unification.
paulson@7290
    75
nipkow@7291
    76
<DT>TLA
nipkow@7291
    77
<DD>Lamport's Temporal Logic of Actions
nipkow@7291
    78
paulson@7290
    79
<DT>Tools
paulson@7290
    80
<DD>holds code used to provide support for records, datatypes, induction, etc.
paulson@7290
    81
paulson@7290
    82
<DT>UNITY
paulson@7290
    83
<DD>Chandy and Misra's UNITY formalism.
nipkow@7291
    84
nipkow@7291
    85
<DT>W0
nipkow@7291
    86
<DD>a precursor of MiniML, without let-expressions
clasohm@1339
    87
</DL>
clasohm@1339
    88
clasohm@1339
    89
Useful references on Higher-Order Logic:
clasohm@1339
    90
clasohm@1339
    91
<UL>
wenzelm@4622
    92
wenzelm@4622
    93
<LI> P. B. Andrews,<BR>
clasohm@1341
    94
    An Introduction to Mathematical Logic and Type Theory<BR>
clasohm@1341
    95
    (Academic Press, 1986).
clasohm@1339
    96
wenzelm@4622
    97
<P>
wenzelm@4622
    98
wenzelm@4622
    99
<LI> A. Church,<BR>
wenzelm@4622
   100
    A Formulation of the Simple Theory of Types<BR>
wenzelm@4622
   101
    (Journal of Symbolic Logic, 1940).
wenzelm@4622
   102
wenzelm@4622
   103
<P>
wenzelm@4622
   104
wenzelm@4622
   105
<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
wenzelm@4622
   106
    Introduction to HOL: A theorem proving environment for higher order logic<BR>
wenzelm@4622
   107
    (Cambridge University Press, 1993).
wenzelm@4622
   108
wenzelm@4622
   109
<P>
wenzelm@4622
   110
wenzelm@4622
   111
<LI> J. Lambek and P. J. Scott,<BR>
wenzelm@4622
   112
    Introduction to Higher Order Categorical Logic<BR>
wenzelm@4622
   113
    (Cambridge University Press, 1986).
wenzelm@4622
   114
clasohm@1339
   115
</UL>
clasohm@1339
   116
clasohm@1339
   117
</BODY></HTML>