src/HOL/README.html
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 36862 952b2b102a0a
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <html>
     4 
     5 <head>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     7   <title>HOL/README</title>
     8 </head>
     9 
    10 <body>
    11 
    12 <h2>HOL: Higher-Order Logic</h2>
    13 
    14 These are the main sources of the Isabelle system for Higher-Order Logic.
    15 
    16 <p>
    17 
    18 There are also several example sessions:
    19 <dl>
    20 
    21 <dt>Algebra
    22 <dd>rings and univariate polynomials
    23 
    24 <dt>Auth
    25 <dd>a new approach to verifying authentication protocols
    26 
    27 <dt>AxClasses
    28 <dd>a few basic examples of using axiomatic type classes
    29 
    30 <dt>Complex
    31 <dd>a development of the complex numbers, the reals, and the hyper-reals,
    32 which are used in non-standard analysis (builds the image HOL-Complex)
    33 
    34 <dt>Hoare
    35 <dd>verification of imperative programs (verification conditions are
    36 generated automatically from pre/post conditions and loop invariants)
    37 
    38 <dt>HoareParallel
    39 <dd>verification of shared-variable imperative programs a la Owicki-Gries.
    40 (verification conditions are generated automatically)
    41 
    42 <dt>Hyperreal
    43 <dd>Nonstandard analysis. Builds on Real and is part of Complex.
    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>Import
    53 <dd>theories imported from other (HOL) theorem provers.
    54 
    55 <dt>Induct
    56 <dd>examples of (co)inductive definitions
    57 
    58 <dt>IOA
    59 <dd>a simple theory of Input/Output Automata
    60 
    61 <dt>Isar_Examples
    62 <dd>several introductory examples using Isabelle/Isar
    63 
    64 <dt>Lambda
    65 <dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
    66 
    67 <dt>Lattice
    68 <dd>lattices and order structures (in Isabelle/Isar)
    69 
    70 <dt>Library
    71 <dd>A collection of generic theories
    72 
    73 <dt>Matrix
    74 <dd>two-dimensional matrices
    75 
    76 <dt>MicroJava
    77 <dd>formalization of a fragment of Java, together with a corresponding
    78 virtual machine and a specification of its bytecode verifier and a
    79 lightweight bytecode verifier, including proofs of type-safety
    80 
    81 <dt>Modelcheck
    82 <dd>basic setup for integration of some model checkers in Isabelle/HOL
    83 
    84 <dt>NanoJava
    85 <dd>Haore Logic for a tiny fragment of Java
    86 
    87 <dt>NumberTheory
    88 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    89 Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
    90 
    91 <dt>Prolog
    92 <dd>a (bare-bones) implementation of Lambda-Prolog
    93 
    94 <dt>Real
    95 <dd>the real numbers, part of Complex
    96 
    97 <dt>Hahn_Banach
    98 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    99 
   100 <dt>SET_Protocol
   101 <dd>verification of the SET Protocol
   102 
   103 <dt>Subst
   104 <dd>a theory of substitution and unification.
   105 
   106 <dt>TLA
   107 <dd>Lamport's Temporal Logic of Actions (with separate example sessions)
   108 
   109 <dt>UNITY
   110 <dd>Chandy and Misra's UNITY formalism
   111 
   112 <dt>W0
   113 <dd>a precursor of MiniML, without let-expressions
   114 
   115 <dt>ex
   116 <dd>miscellaneous examples
   117 
   118 </dl>
   119 
   120 </body>
   121 </html>