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