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