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