README
1This is the examples directory.
2
3Currently here are the following:
4
5
6 * ARM
7
8 This directory contains a formal model of the ARM6
9 processor core (which implements v3 of the ARM architecture),
10 along with a proof of correctness. The specifications and
11 proofs are due to Anthony Fox, and arise from a collaboration
12 between Cambridge, Leeds and ARM.
13
14 * autopilot.sml
15
16 This example is a rendition of a PVS example due to Ricky
17 Butler of NASA. The example shows the use of a record-definition
18 package due to Mike Norrish and Phil Windley, as well as
19 illustrating some aspects of the automation currently available
20 in HOL.
21
22 * bmark
23
24 This example is an old and standard HOL benchmark: the proof of
25 correctness of a multiplier circuit, due to Mike Gordon.
26
27 * computability
28
29 Some basic computability theory, based on two models: the
30 lambda-calculus and the recursive functions. These are proved
31 equivalent. Results include Rice's theorem, and that if a set
32 and its complement are r.e., then they are also recursive.
33
34 * CCS
35
36 This directory contains a formalization of the Process Algebra CCS.
37 (Milner's Calculus of Communicating Systems)
38 Author: Monica Nesi (ported from HOL88 by Chun Tian)
39
40 * Crypto
41
42 This directory holds a formalization of a number of different
43 crypto-systems, including Rijmen and Daemen's AES crypto
44 standard, together with a proof of correctness.
45
46 * euclid.sml
47
48 This example is a proof of Euclid's theorem on the infinitude of
49 the prime numbers. It has been extracted and modified by Konrad
50 Slind from a much larger development originally due to John
51 Harrison.
52
53 * fol.sml
54
55 This file exercises John Harrison's implementation of a
56 model-elimination style first order prover.
57
58 * ind_def
59
60 This directory contains some examples of Tom Melham's inductive
61 definition package in action. Featured are an operational
62 semantics for a small imperative programming language, a small
63 process algebra, and combinatory logic with its type system. The
64 files are extensively commented.
65
66 * lambda
67
68 This directory contains a variety of theories about the lambda
69 calculus, including multiple models (nominal, de Bruijn,
70 locally nameless) and results such as confluence and
71 standardisation.
72
73 * miller
74
75 This example is a verification of the Miller-Rabin
76 probabilistic primality test, incorporating version 2 of
77 probability theory and some cute example probabilistic
78 programs. Author: Joe Hurd.
79
80 * MLSyntax
81
82 This example shows the use of a facility for defining
83 recursive types, implemented by John Harrison. In the example,
84 due to Elsa Gunter, the abstract syntax for a small but not
85 totally unrealistic subset of ML is defined, along with a simple
86 mutually recursive function over the syntax.
87
88 * ordinal
89
90 This directory contains a formalization of the ordinals up to �����
91 and proves corresponding induction and recursion theorems.
92
93 * PropLogic
94
95 This file contains a development of propositional logic, up
96 to the completeness theorem.
97
98 * PSL
99
100 This directory contains a deep embedding of the Accellera
101 standard property language Sugar 2.0. Author: Mike Gordon.
102
103 * ring.sml
104
105 Application of normalization and decision procedures for rings.
106 Author: Bruno Barras.
107
108 * root2.sml
109
110 A proof that the square root of two is not rational. Adapted
111 from a proof by John Harrison.
112
113 * RSA
114
115 This directory develops some of the mathematics underlying
116 the RSA cryptography scheme. The theories have been
117 produced by Laurent Thery of INRIA Sophia-Antipolis.
118
119 * taut.sml
120
121 This file presents some tautologies, and uses an ML binding of
122 J"orn Lind's ROBDD (Reduced Ordered Binary Decision Diagram) package
123 to attempt to prove them.
124
125 * tempScript.sml
126
127 This file is a template for making a separately compilable HOL
128 theory script.
129
130 * Thery
131
132 This file is a very simple introductory example of proof in HOL,
133 extracted from
134
135 "A quick overview of PVS and HOL"
136
137 by Laurent Thery of INRIA, Sophia-Antipolis, which was presented
138 at
139
140 "Types summer school'99: Theory and practice of formal proofs",
141 Giens, France, August 30 - September 10, 1999.
142
143