10163

1 
<html>


2 

2080

3 
<! $Id$ >

1339

4 

10163

5 
<head><title>HOL/README</title></head>

1339

6 

10163

7 
<body>


8 


9 
<h2>HOL: HigherOrder Logic</h2>

1339

10 

10262

11 
These are the main sources of the Isabelle system for HigherOrder Logic.

10163

12 


13 
<p>

2080

14 

10163

15 
There are also several example sessions:


16 
<dl>

2080

17 

10163

18 
<dt>Algebra


19 
<dd>rings and univariate polynomials


20 


21 
<dt>Auth


22 
<dd>a new approach to verifying authentication protocols

7303

23 

10163

24 
<dt>AxClasses


25 
<dd>a few basic examples of using axiomatic type classes


26 


27 
<dt>BCV


28 
<dd>generic model of bytecode verification, i.e. dataflow analysis


29 
for assembly languages with subtypes

7303

30 

10163

31 
<dt>HOLReal


32 
<dd>a development of the reals and hyperreals, which are used in


33 
nonstandard analysis (builds the image HOLReal)

7303

34 

10163

35 
<dt>HOLRealHahnBanach


36 
<dd>the HahnBanach theorem for real vector spaces (in Isabelle/Isar)

7303

37 

10163

38 
<dt>HOLRealex


39 
<dd>miscellaneous real number examples


40 


41 
<dt>Hoare


42 
<dd>verification of imperative programs (verification conditions are


43 
generated automatically from pre/post conditions and loop invariants)

7691

44 

10163

45 
<dt>IMP


46 
<dd>mechanization of a large part of a semantics text by Glynn Winskel

7291

47 

10163

48 
<dt>IMPP


49 
<dd>extension of IMP with local variables and mutually recursive


50 
procedures

2080

51 

10163

52 
<dt>IOA


53 
<dd>a simple theory of Input/Output Automata


54 


55 
<dt>Induct


56 
<dd>examples of (co)inductive definitions

3125

57 

10163

58 
<dt>Isar_examples


59 
<dd>several introductory examples using Isabelle/Isar

2080

60 

10163

61 
<dt>Lambda


62 
<dd>fundamental properties of lambdacalculus (ChurchRosser and termination)

2080

63 

10163

64 
<dt>Lattice


65 
<dd>lattices and order structures (in Isabelle/Isar)

7303

66 

10163

67 
<dt>Lex


68 
<dd>verification of a simple lexical analyzer generator

1339

69 

10163

70 
<dt>MicroJava


71 
<dd>formalization of a fragment of Java, together with a corresponding


72 
virtual machine and a specification of its bytecode verifier and a


73 
lightweight bytecode verifier, including proofs of typesafety.

7291

74 

10163

75 
<dt>MiniML


76 
<dd>formalization of type inference for the language MiniML

7291

77 

10163

78 
<dt>Modelcheck


79 
<dd>basic setup for integration of some model checkers in Isabelle/HOL

7290

80 

10163

81 
<dt>NumberTheory


82 
<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,


83 
Fermat/Euler Theorem, Wilson's Theorem

7662

84 

10163

85 
<dt>Prolog


86 
<dd>a (barebones) implementation of LambdaProlog


87 


88 
<dt>Subst


89 
<dd>defines a theory of substitution and unification.

7290

90 

10163

91 
<dt>TLA


92 
<dd>Lamport's Temporal Logic of Actions (with separate example sessions)

7291

93 

10163

94 
<dt>UNITY


95 
<dd>Chandy and Misra's UNITY formalism

7290

96 

10163

97 
<dt>W0


98 
<dd>a precursor of MiniML, without letexpressions

7291

99 

10163

100 
<dt>ex


101 
<dd>miscellaneous examples


102 


103 
</dl>

1339

104 


105 
Useful references on HigherOrder Logic:


106 

10163

107 
<ul>

1339

108 

10163

109 
<li>P. B. Andrews,<br>


110 
An Introduction to Mathematical Logic and Type Theory<br>


111 
(Academic Press, 1986).

4622

112 

10163

113 
<li>A. Church,<br>


114 
A Formulation of the Simple Theory of Types<br>


115 
(Journal of Symbolic Logic, 1940).

4622

116 

10163

117 
<li>M. J. C. Gordon and T. F. Melham (editors),<br>


118 
Introduction to HOL: A theorem proving environment for higher order logic<br>


119 
(Cambridge University Press, 1993).

4622

120 

10163

121 
<li>J. Lambek and P. J. Scott,<br>


122 
Introduction to Higher Order Categorical Logic<br>


123 
(Cambridge University Press, 1986).

4622

124 

10163

125 
</ul>

1339

126 

10163

127 
</body>


128 
</html>
