src/HOL/README.html
changeset 10163 d1972b445ece
parent 9811 39ffdb8cab03
child 10262 3c43e8086cba
     1.1 --- a/src/HOL/README.html	Fri Oct 06 16:11:53 2000 +0200
     1.2 +++ b/src/HOL/README.html	Fri Oct 06 16:14:03 2000 +0200
     1.3 @@ -1,117 +1,129 @@
     1.4 +<html>
     1.5 +
     1.6  <!-- $Id$ -->
     1.7 -<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
     1.8  
     1.9 -<H2>HOL: Higher-Order Logic</H2>
    1.10 +<head><title>HOL/README</title></head>
    1.11  
    1.12 -This directory contains the ML sources of the Isabelle system for
    1.13 -Higher-Order Logic.<P>
    1.14 +<body>
    1.15 +
    1.16 +<h2>HOL: Higher-Order Logic</h2>
    1.17  
    1.18 -There are several subdirectories with examples:
    1.19 -<DL>
    1.20 -<DT>ex
    1.21 -<DD>general examples
    1.22 +This directory contains the sources of the Isabelle system for
    1.23 +Higher-Order Logic.
    1.24 +
    1.25 +<p>
    1.26  
    1.27 -<DT>Auth
    1.28 -<DD>a new approach to verifying authentication protocols 
    1.29 +There are also several example sessions:
    1.30 +<dl>
    1.31  
    1.32 -<DT>AxClasses
    1.33 -<DD>a few axiomatic type class examples:
    1.34 -<DL>
    1.35 +<dt>Algebra
    1.36 +<dd>rings and univariate polynomials
    1.37 +
    1.38 +<dt>Auth
    1.39 +<dd>a new approach to verifying authentication protocols
    1.40  
    1.41 -<DT> Tutorial <DD> Some simple axclass demos that go along with the
    1.42 -<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
    1.43 +<dt>AxClasses
    1.44 +<dd>a few basic examples of using axiomatic type classes
    1.45 +
    1.46 +<dt>BCV
    1.47 +<dd>generic model of bytecode verification, i.e. data-flow analysis
    1.48 +for assembly languages with subtypes
    1.49  
    1.50 -<DT> Group
    1.51 -<DD> Some bits of group theory.
    1.52 +<dt>HOL-Real
    1.53 +<dd>a development of the reals and hyper-reals, which are used in
    1.54 +non-standard analysis (builds the image HOL-Real)
    1.55  
    1.56 -<DT> Lattice
    1.57 -<DD> Basic theory of lattices and orders.
    1.58 -
    1.59 -</DL>
    1.60 +<dt>HOL-Real-HahnBanach
    1.61 +<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    1.62  
    1.63 -<DT>BCV
    1.64 -<DD>generic model of bytecode verification, i.e. data-flow analysis
    1.65 -for assembly languages with subtypes.
    1.66 +<dt>HOL-Real-ex
    1.67 +<dd>miscellaneous real number examples
    1.68 +
    1.69 +<dt>Hoare
    1.70 +<dd>verification of imperative programs (verification conditions are
    1.71 +generated automatically from pre/post conditions and loop invariants)
    1.72  
    1.73 -<DT>Hoare
    1.74 -<DD>verification of imperative programs; verification conditions are
    1.75 -generated automatically from pre/post conditions and loop invariants.
    1.76 +<dt>IMP
    1.77 +<dd>mechanization of a large part of a semantics text by Glynn Winskel
    1.78  
    1.79 -<DT>IMP
    1.80 -<DD>mechanization of a large part of a semantics text by Glynn Winskel
    1.81 +<dt>IMPP
    1.82 +<dd>extension of IMP with local variables and mutually recursive
    1.83 +procedures
    1.84  
    1.85 -<DT>Induct
    1.86 -<DD>examples of (co)inductive definitions
    1.87 +<dt>IOA
    1.88 +<dd>a simple theory of Input/Output Automata
    1.89 +
    1.90 +<dt>Induct
    1.91 +<dd>examples of (co)inductive definitions
    1.92  
    1.93 -<DT>Integ 
    1.94 -<DD>a development of the integers including efficient integer
    1.95 -calculations (part of the standard HOL environment)
    1.96 +<dt>Isar_examples
    1.97 +<dd>several introductory examples using Isabelle/Isar
    1.98  
    1.99 -<DT>IOA
   1.100 -<DD>a simple theory of Input/Output Automata
   1.101 +<dt>Lambda
   1.102 +<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
   1.103  
   1.104 -<DT>Isar_examples
   1.105 -<DD>several introductory Isabelle/Isar examples
   1.106 +<dt>Lattice
   1.107 +<dd>lattices and order structures (in Isabelle/Isar)
   1.108  
   1.109 -<DT>Lambda
   1.110 -<DD>fundamental properties of lambda-calculus (Church-Rosser and termination)
   1.111 +<dt>Lex
   1.112 +<dd>verification of a simple lexical analyzer generator
   1.113  
   1.114 -<DT>Lex
   1.115 -<DD>verification of a simple lexical analyzer generator
   1.116 +<dt>MicroJava
   1.117 +<dd>formalization of a fragment of Java, together with a corresponding
   1.118 +virtual machine and a specification of its bytecode verifier and a
   1.119 +lightweight bytecode verifier, including proofs of type-safety.
   1.120  
   1.121 -<DT>MiniML
   1.122 -<DD>formalization of type inference for the language Mini-ML
   1.123 +<dt>MiniML
   1.124 +<dd>formalization of type inference for the language Mini-ML
   1.125  
   1.126 -<DT>Real 
   1.127 -<DD>a development of the reals and hyper-reals, which are used in
   1.128 -non-standard analysis.  Also includes the positive rationals.  Used to build
   1.129 -the image HOL-Real.
   1.130 +<dt>Modelcheck
   1.131 +<dd>basic setup for integration of some model checkers in Isabelle/HOL
   1.132  
   1.133 -<DT>Real/HahnBanach
   1.134 -<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
   1.135 +<dt>NumberTheory
   1.136 +<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
   1.137 +Fermat/Euler Theorem, Wilson's Theorem
   1.138  
   1.139 -<DT>Subst
   1.140 -<DD>defines a theory of substitution and unification.
   1.141 +<dt>Prolog
   1.142 +<dd>a (bare-bones) implementation of Lambda-Prolog
   1.143 +
   1.144 +<dt>Subst
   1.145 +<dd>defines a theory of substitution and unification.
   1.146  
   1.147 -<DT>TLA
   1.148 -<DD>Lamport's Temporal Logic of Actions
   1.149 +<dt>TLA
   1.150 +<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
   1.151  
   1.152 -<DT>Tools
   1.153 -<DD>holds code used to provide support for records, datatypes, induction, etc.
   1.154 +<dt>UNITY
   1.155 +<dd>Chandy and Misra's UNITY formalism
   1.156  
   1.157 -<DT>UNITY
   1.158 -<DD>Chandy and Misra's UNITY formalism.
   1.159 +<dt>W0
   1.160 +<dd>a precursor of MiniML, without let-expressions
   1.161  
   1.162 -<DT>W0
   1.163 -<DD>a precursor of MiniML, without let-expressions
   1.164 -</DL>
   1.165 +<dt>ex
   1.166 +<dd>miscellaneous examples
   1.167 +
   1.168 +</dl>
   1.169  
   1.170  Useful references on Higher-Order Logic:
   1.171  
   1.172 -<UL>
   1.173 -
   1.174 -<LI> P. B. Andrews,<BR>
   1.175 -    An Introduction to Mathematical Logic and Type Theory<BR>
   1.176 -    (Academic Press, 1986).
   1.177 +<ul>
   1.178  
   1.179 -<P>
   1.180 +<li>P. B. Andrews,<br>
   1.181 +An Introduction to Mathematical Logic and Type Theory<br>
   1.182 +(Academic Press, 1986).
   1.183  
   1.184 -<LI> A. Church,<BR>
   1.185 -    A Formulation of the Simple Theory of Types<BR>
   1.186 -    (Journal of Symbolic Logic, 1940).
   1.187 -
   1.188 -<P>
   1.189 +<li>A. Church,<br>
   1.190 +A Formulation of the Simple Theory of Types<br>
   1.191 +(Journal of Symbolic Logic, 1940).
   1.192  
   1.193 -<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
   1.194 -    Introduction to HOL: A theorem proving environment for higher order logic<BR>
   1.195 -    (Cambridge University Press, 1993).
   1.196 -
   1.197 -<P>
   1.198 +<li>M. J. C. Gordon and T. F. Melham (editors),<br>
   1.199 +Introduction to HOL: A theorem proving environment for higher order logic<br>
   1.200 +(Cambridge University Press, 1993).
   1.201  
   1.202 -<LI> J. Lambek and P. J. Scott,<BR>
   1.203 -    Introduction to Higher Order Categorical Logic<BR>
   1.204 -    (Cambridge University Press, 1986).
   1.205 +<li>J. Lambek and P. J. Scott,<br>
   1.206 +Introduction to Higher Order Categorical Logic<br>
   1.207 +(Cambridge University Press, 1986).
   1.208  
   1.209 -</UL>
   1.210 +</ul>
   1.211  
   1.212 -</BODY></HTML>
   1.213 +</body>
   1.214 +</html>