src/HOL/README.html
author webertj
Mon Mar 07 19:17:07 2005 +0100 (2005-03-07)
changeset 15582 7219facb3fd0
parent 15283 f21466450330
child 15910 5df57194d064
permissions -rw-r--r--
HTML 4.01 Transitional conformity
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <html>
     6 
     7 <head>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <title>HOL/README</title>
    10 </head>
    11 
    12 <body>
    13 
    14 <h2>HOL: Higher-Order Logic</h2>
    15 
    16 These are the main sources of the Isabelle system for Higher-Order Logic.
    17 
    18 <p>
    19 
    20 There are also several example sessions:
    21 <dl>
    22 
    23 <dt>Algebra
    24 <dd>rings and univariate polynomials
    25 
    26 <dt>Auth
    27 <dd>a new approach to verifying authentication protocols
    28 
    29 <dt>AxClasses
    30 <dd>a few basic examples of using axiomatic type classes
    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>HOL-Complex
    37 <dd>a development of the complex numbers, the reals, and the hyper-reals,
    38 which are used in non-standard analysis (builds the image HOL-Complex)
    39 
    40 <dt>HOL-Complex-HahnBanach
    41 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    42 
    43 <dt>HOL-Complex-ex
    44 <dd>miscellaneous real ans complex number examples
    45 
    46 <dt>Hoare
    47 <dd>verification of imperative programs (verification conditions are
    48 generated automatically from pre/post conditions and loop invariants)
    49 
    50 <dt>IMP
    51 <dd>mechanization of a large part of a semantics text by Glynn Winskel
    52 
    53 <dt>IMPP
    54 <dd>extension of IMP with local variables and mutually recursive
    55 procedures
    56 
    57 <dt>IOA
    58 <dd>a simple theory of Input/Output Automata
    59 
    60 <dt>Induct
    61 <dd>examples of (co)inductive definitions
    62 
    63 <dt>Isar_examples
    64 <dd>several introductory examples using Isabelle/Isar
    65 
    66 <dt>Lambda
    67 <dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
    68 
    69 <dt>Lattice
    70 <dd>lattices and order structures (in Isabelle/Isar)
    71 
    72 <dt>MicroJava
    73 <dd>formalization of a fragment of Java, together with a corresponding
    74 virtual machine and a specification of its bytecode verifier and a
    75 lightweight bytecode verifier, including proofs of type-safety.
    76 
    77 <dt>Modelcheck
    78 <dd>basic setup for integration of some model checkers in Isabelle/HOL
    79 
    80 <dt>NumberTheory
    81 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    82 Fermat/Euler Theorem, Wilson's Theorem
    83 
    84 <dt>Prolog
    85 <dd>a (bare-bones) implementation of Lambda-Prolog
    86 
    87 <dt>Subst
    88 <dd>defines a theory of substitution and unification.
    89 
    90 <dt>TLA
    91 <dd>Lamport's Temporal Logic of Actions (with separate example sessions)
    92 
    93 <dt>UNITY
    94 <dd>Chandy and Misra's UNITY formalism
    95 
    96 <dt>W0
    97 <dd>a precursor of MiniML, without let-expressions
    98 
    99 <dt>ex
   100 <dd>miscellaneous examples
   101 
   102 </dl>
   103 
   104 Useful references on Higher-Order Logic:
   105 
   106 <ul>
   107 
   108 <li>P. B. Andrews,<br>
   109 An Introduction to Mathematical Logic and Type Theory<br>
   110 (Academic Press, 1986).
   111 
   112 <li>A. Church,<br>
   113 A Formulation of the Simple Theory of Types<br>
   114 (Journal of Symbolic Logic, 1940).
   115 
   116 <li>M. J. C. Gordon and T. F. Melham (editors),<br>
   117 Introduction to HOL: A theorem proving environment for higher order logic<br>
   118 (Cambridge University Press, 1993).
   119 
   120 <li>J. Lambek and P. J. Scott,<br>
   121 Introduction to Higher Order Categorical Logic<br>
   122 (Cambridge University Press, 1986).
   123 
   124 </ul>
   125 
   126 </body>
   127 </html>