src/HOL/README.html
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14543 0e266a5dd6e3
child 15283 f21466450330
permissions -rw-r--r--
import -> imports
     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-Complex
    32 <dd>a development of the complex numbers, the reals, and the hyper-reals,
    33 which are used in non-standard analysis (builds the image HOL-Complex)
    34 
    35 <dt>HOL-Complex-HahnBanach
    36 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    37 
    38 <dt>HOL-Complex-ex
    39 <dd>miscellaneous real ans complex 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>MicroJava
    68 <dd>formalization of a fragment of Java, together with a corresponding
    69 virtual machine and a specification of its bytecode verifier and a
    70 lightweight bytecode verifier, including proofs of type-safety.
    71 
    72 <dt>Modelcheck
    73 <dd>basic setup for integration of some model checkers in Isabelle/HOL
    74 
    75 <dt>NumberTheory
    76 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    77 Fermat/Euler Theorem, Wilson's Theorem
    78 
    79 <dt>Prolog
    80 <dd>a (bare-bones) implementation of Lambda-Prolog
    81 
    82 <dt>Subst
    83 <dd>defines a theory of substitution and unification.
    84 
    85 <dt>TLA
    86 <dd>Lamport's Temporal Logic of Actions (with separate example sessions)
    87 
    88 <dt>UNITY
    89 <dd>Chandy and Misra's UNITY formalism
    90 
    91 <dt>W0
    92 <dd>a precursor of MiniML, without let-expressions
    93 
    94 <dt>ex
    95 <dd>miscellaneous examples
    96 
    97 </dl>
    98 
    99 Useful references on Higher-Order Logic:
   100 
   101 <ul>
   102 
   103 <li>P. B. Andrews,<br>
   104 An Introduction to Mathematical Logic and Type Theory<br>
   105 (Academic Press, 1986).
   106 
   107 <li>A. Church,<br>
   108 A Formulation of the Simple Theory of Types<br>
   109 (Journal of Symbolic Logic, 1940).
   110 
   111 <li>M. J. C. Gordon and T. F. Melham (editors),<br>
   112 Introduction to HOL: A theorem proving environment for higher order logic<br>
   113 (Cambridge University Press, 1993).
   114 
   115 <li>J. Lambek and P. J. Scott,<br>
   116 Introduction to Higher Order Categorical Logic<br>
   117 (Cambridge University Press, 1986).
   118 
   119 </ul>
   120 
   121 </body>
   122 </html>