This is the examples directory.

Currently here are the following:


  * ARM

       This directory contains a formal model of the ARM6
       processor core (which implements v3 of the ARM architecture),
       along with a proof of correctness.  The specifications and
       proofs are due to Anthony Fox, and arise from a collaboration
       between Cambridge, Leeds and ARM.

  * autopilot.sml

       This example is a rendition of a PVS example due to Ricky
       Butler of NASA. The example shows the use of a record-definition
       package due to Mike Norrish and Phil Windley, as well as
       illustrating some aspects of the automation currently available
       in HOL.

  * bmark

       This example is an old and standard HOL benchmark: the proof of
       correctness of a multiplier circuit, due to Mike Gordon.

  * computability

       Some basic computability theory, based on two models: the
       lambda-calculus and the recursive functions.  These are proved
       equivalent.  Results include Rice's theorem, and that if a set
       and its complement are r.e., then they are also recursive.

  * CCS

       This directory contains a formalization of the Process Algebra CCS.
       (Milner's Calculus of Communicating Systems)
       Author: Monica Nesi (ported from HOL88 by Chun Tian)

  * Crypto

       This directory holds a formalization of a number of different
       crypto-systems, including Rijmen and Daemen's AES crypto
       standard, together with a proof of correctness.

  * euclid.sml

       This example is a proof of Euclid's theorem on the infinitude of
       the prime numbers. It has been extracted and modified by Konrad
       Slind from a much larger development originally due to John
       Harrison.

  * fol.sml

       This file exercises John Harrison's implementation of a
       model-elimination style first order prover.

  * ind_def

       This directory contains some examples of Tom Melham's inductive
       definition package in action. Featured are an operational
       semantics for a small imperative programming language, a small
       process algebra, and combinatory logic with its type system. The
       files are extensively commented.

  * lambda

       This directory contains a variety of theories about the lambda
       calculus, including multiple models (nominal, de Bruijn,
       locally nameless) and results such as confluence and
       standardisation.

  * miller

       This example is a verification of the Miller-Rabin
       probabilistic primality test, incorporating version 2 of
       probability theory and some cute example probabilistic
       programs. Author: Joe Hurd.

  * MLSyntax

       This example shows the use of a facility for defining
       recursive types, implemented by John Harrison. In the example,
       due to Elsa Gunter, the abstract syntax for a small but not
       totally unrealistic subset of ML is defined, along with a simple
       mutually recursive function over the syntax.

  * ordinal

      This directory contains a formalization of the ordinals up to ε₀
      and proves corresponding induction and recursion theorems.

  * PropLogic

      This file contains a development of propositional logic, up
      to the completeness theorem.

  * PSL

       This directory contains a deep embedding of the Accellera
       standard property language Sugar 2.0. Author: Mike Gordon.

  * ring.sml

       Application of normalization and decision procedures for rings.
       Author: Bruno Barras.

  * root2.sml

       A proof that the square root of two is not rational. Adapted
       from a proof by John Harrison.

  * RSA

       This directory develops some of the mathematics underlying
       the RSA cryptography scheme. The theories have been
       produced by Laurent Thery of INRIA Sophia-Antipolis.

  * taut.sml

       This file presents some tautologies, and uses an ML binding of
       J"orn Lind's ROBDD (Reduced Ordered Binary Decision Diagram) package
       to attempt to prove them.

  * tempScript.sml

       This file is a template for making a separately compilable HOL
       theory script.

  * Thery

       This file is a very simple introductory example of proof in HOL,
       extracted from

         "A quick overview of PVS and HOL"

       by Laurent Thery of INRIA, Sophia-Antipolis, which was presented
       at

         "Types summer school'99: Theory and practice of formal proofs",
         Giens, France, August 30 - September 10, 1999.