src/HOL/README.html
author wenzelm
Sat Sep 02 21:56:24 2000 +0200 (2000-09-02)
changeset 9811 39ffdb8cab03
parent 7983 d823fdcc0645
child 10163 d1972b445ece
permissions -rw-r--r--
HOL/Lambda: converted into new-style theory and document;
     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>BCV
    33 <DD>generic model of bytecode verification, i.e. data-flow analysis
    34 for assembly languages with subtypes.
    35 
    36 <DT>Hoare
    37 <DD>verification of imperative programs; verification conditions are
    38 generated automatically from pre/post conditions and loop invariants.
    39 
    40 <DT>IMP
    41 <DD>mechanization of a large part of a semantics text by Glynn Winskel
    42 
    43 <DT>Induct
    44 <DD>examples of (co)inductive definitions
    45 
    46 <DT>Integ 
    47 <DD>a development of the integers including efficient integer
    48 calculations (part of the standard HOL environment)
    49 
    50 <DT>IOA
    51 <DD>a simple theory of Input/Output Automata
    52 
    53 <DT>Isar_examples
    54 <DD>several introductory Isabelle/Isar examples
    55 
    56 <DT>Lambda
    57 <DD>fundamental properties of lambda-calculus (Church-Rosser and termination)
    58 
    59 <DT>Lex
    60 <DD>verification of a simple lexical analyzer generator
    61 
    62 <DT>MiniML
    63 <DD>formalization of type inference for the language Mini-ML
    64 
    65 <DT>Real 
    66 <DD>a development of the reals and hyper-reals, which are used in
    67 non-standard analysis.  Also includes the positive rationals.  Used to build
    68 the image HOL-Real.
    69 
    70 <DT>Real/HahnBanach
    71 <DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
    72 
    73 <DT>Subst
    74 <DD>defines a theory of substitution and unification.
    75 
    76 <DT>TLA
    77 <DD>Lamport's Temporal Logic of Actions
    78 
    79 <DT>Tools
    80 <DD>holds code used to provide support for records, datatypes, induction, etc.
    81 
    82 <DT>UNITY
    83 <DD>Chandy and Misra's UNITY formalism.
    84 
    85 <DT>W0
    86 <DD>a precursor of MiniML, without let-expressions
    87 </DL>
    88 
    89 Useful references on Higher-Order Logic:
    90 
    91 <UL>
    92 
    93 <LI> P. B. Andrews,<BR>
    94     An Introduction to Mathematical Logic and Type Theory<BR>
    95     (Academic Press, 1986).
    96 
    97 <P>
    98 
    99 <LI> A. Church,<BR>
   100     A Formulation of the Simple Theory of Types<BR>
   101     (Journal of Symbolic Logic, 1940).
   102 
   103 <P>
   104 
   105 <LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
   106     Introduction to HOL: A theorem proving environment for higher order logic<BR>
   107     (Cambridge University Press, 1993).
   108 
   109 <P>
   110 
   111 <LI> J. Lambek and P. J. Scott,<BR>
   112     Introduction to Higher Order Categorical Logic<BR>
   113     (Cambridge University Press, 1986).
   114 
   115 </UL>
   116 
   117 </BODY></HTML>