Fetching latest commit…
Cannot retrieve the latest commit at this time.
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. * 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.