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