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