src/HOL/README.html
author wenzelm
Thu Sep 30 20:49:06 1999 +0200 (1999-09-30)
changeset 7662 062a782d7402
parent 7303 96bc013c8987
child 7691 b7e8277fa088
permissions -rw-r--r--
Real/HahnBanach;
     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>several Isabelle/Isar example 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>Real/HahnBanach
    67 <DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
    68 
    69 <DT>Subst
    70 <DD>defines a theory of substitution and unification.
    71 
    72 <DT>TLA
    73 <DD>Lamport's Temporal Logic of Actions
    74 
    75 <DT>Tools
    76 <DD>holds code used to provide support for records, datatypes, induction, etc.
    77 
    78 <DT>UNITY
    79 <DD>Chandy and Misra's UNITY formalism.
    80 
    81 <DT>W0
    82 <DD>a precursor of MiniML, without let-expressions
    83 </DL>
    84 
    85 Useful references on Higher-Order Logic:
    86 
    87 <UL>
    88 
    89 <LI> P. B. Andrews,<BR>
    90     An Introduction to Mathematical Logic and Type Theory<BR>
    91     (Academic Press, 1986).
    92 
    93 <P>
    94 
    95 <LI> A. Church,<BR>
    96     A Formulation of the Simple Theory of Types<BR>
    97     (Journal of Symbolic Logic, 1940).
    98 
    99 <P>
   100 
   101 <LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
   102     Introduction to HOL: A theorem proving environment for higher order logic<BR>
   103     (Cambridge University Press, 1993).
   104 
   105 <P>
   106 
   107 <LI> J. Lambek and P. J. Scott,<BR>
   108     Introduction to Higher Order Categorical Logic<BR>
   109     (Cambridge University Press, 1986).
   110 
   111 </UL>
   112 
   113 </BODY></HTML>