Automated Reasoning Group

The History of the HOL System

(Based on the preface to the HOL system Description.)

The HOL System is designed to support interactive theorem proving in higher order logic (hence the acronym `HOL'). To this end, the formal logic is interfaced to a general purpose programming language (ML, for meta-language) in which terms and theorems of the logic can be denoted, proof strategies expressed and applied, and logical theories developed.

The version of higher order logic used in HOL is predicate calculus with terms from the typed lambda calculus (i.e. simple type theory). This was originally developed as a foundation for mathematics [1]. The primary application area of HOL was initially intended to be the specification and verification of hardware designs. (The use of higher order logic for this purpose was first advocated by Keith Hanna [2].) However, the logic does not restrict applications to hardware; HOL has been applied to many other areas.

The approach to mechanizing formal proof used in HOL is due to Robin Milner [3], who also headed the team that designed and implemented the language ML. That work centred on a system called LCF (logic for computable functions), which was intended for interactive automated reasoning about higher order recursively defined functions. The interface of the logic to the meta-language was made explicit, using the type structure of ML, with the intention that other logics eventually be tried in place of the original logic. The HOL system is a direct descendant of LCF; this is reflected in everything from its structure and outlook to its incorporation of ML, and even to parts of its implementation. Thus HOL satisfies the early plan to apply the LCF methodology to other logics.

The original LCF was implemented at Edinburgh in the early 1970's, and is now referred to as `Edinburgh LCF'. Its code was ported from Stanford Lisp to Franz Lisp by Gérard Huet at INRIA, and was used in a French research project called `Formel'. Huet's Franz Lisp version of LCF was further developed at Cambridge by Larry Paulson, and became known as `Cambridge LCF'. The HOL system is implemented on top of an early version of Cambridge LCF and consequently many features of both Edinburgh and Cambridge LCF were inherited by HOL. For example, the axiomatization of higher order logic used is not the classical one due to Church, but an equivalent formulation influenced by LCF.

The language ML has now achieved status as a programming language in its own right, although it was originally designed as the proof management language for LCF. It is a functional language distinguished particularly for its type inference mechanism, that gives type security without overburdening the user. Types, and especially abstract types, are the basis for distinguishing the theorems of a logic from arbitrary formulae, in a secure way. A standard has now been established for ML [4]. The most recent version of Cambridge LCF, which is documented in Paulson's book [5], is based on this Standard ML.

The original HOL system included an earlier version of ML, as did the enhanced and rationalized version, called HOL88, which was released (in 1988) after the original HOL system had been in use for several years.

In the early 1990's HOL90, an implementation of HOL based on Standard ML rather than Lisp, was developed by Konrad Slind, initially at the University of Calgary. A commercial version of HOL using Standard ML was also developed by ICL Secure Systems. This system, now called ProofPower, is a `highly assured' system for commercial verification projects in the safety and security critical areas.

References

  1. A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic Vol. 5 (1940), pp. 56-68.
  2. F. K. Hanna and N. Daeche, "Specification and Verification Using Higher-Order Logic: A Case Study". In Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI, edited by G. Milne and P. A. Subrahmanyam, North-Holland, 1986, pp. 179-213.
  3. M. Gordon, R. Milner and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, Vol. 78, Springer-Verlag, 1979.
  4. R. Milner, M. Tofte and R. Harper, The Definition of Standard ML, The MIT Press, 1990.
  5. L. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Tracts in Theoretical Computer Science 2, Cambridge University Press, 1987.

Systems Related to HOL

There are a number of theorem proving systems related to the HOL System; some of them are listed below. Carolyn Talcott and Michael Kohlhase have put together a page on mechanized reasoning.

ACL2
ACL2 is a theorem proving system produced at Computational Logic, Inc. The acronym ``ACL2'' stands for ``A Computational Logic for Applicative Common Lisp.'' ACL2 is similar to the Boyer-Moore theorem prover, Nqthm, and Kaufmann's interactive extension, Pc-Nqthm. However, instead of supporting the ``Boyer-Moore logic,'' ACL2 supports a large applicative subset of Common Lisp. Furthermore, ACL2 is programmed almost entirely within that language.

CLAM
CLAM is a proof planner from the Mathematical Reasoning Group at the Department of Artificial Intelligence, University of Edinburgh.

Coq
The Coq proof assistant allows mechanical manipulation of assertions of the "Calculus of Inductive Constructions", interactive development of formal proofs, and synthesis of certified programs from the constructive proofs of their specifications.

Eves
Eves is a verification environment, the main component of which is a theorem prover called Never.

Gypsy
Gypsy is a verification environment with its own language.

Hol Light
HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel.

Isabelle
Isabelle is a generic theorem prover written in Standard ML. It is generic in the sense that users can define their own logic using a metalogic. Isabelle has a number of things in common with HOL: a programming meta-language, tactics and tacticals, and a fully-expanded proof is generated (over time). There are also significant differences, e.g., rules are not implemented as ML functions but are represented as explicit structures, and higher-order resolution is used for proof construction.

LAMBDA
LAMBDA is a commercial system similar to Isabelle but specialised to a classical higher-order logic with polymorphism like the one mechanised in the HOL system. Early versions implemented a constructive logic of partial terms. The system comes with a graphical interface for hardware design called DIALOG.

LP
The Larch Prover is an interactive theorem proving system for multisorted first-order logic.

Nqthm (The Boyer-Moore Theorem Prover)
Nqthm is a theorem proving system for a computational logic. The logic is (intentionally) similar to the core of the Lisp programming language. It is untyped, quantifier free, and first order. Nqthm provides a high degree of automation in terms of heuristics for simplification, induction, and related activities. A proof in the system is generated by making definitions and then calling the heuristics on the conjecture to be proved. The proof attempt will typically fail, but examination of the prover's log (which is in English) will reveal either a flaw in the conjecture or a lemma that the prover needs to be aware of to succeed. The user then asks the system to prove this lemma (possibly requiring other lemmas to be proved) and repeats the attempt to prove the original conjecture. This process continues until the prover succeeds on the conjecture.

Nuprl
Nuprl is another system descended from LCF. Its logic is based on Martin-Löf's intuitionistic (constructive) type theory. The infrastructure of Nuprl has much in common with HOL, but differs in that proofs are represented explicitly as objects. However, these are not full proofs in terms of primitive inferences; each node of the proof tree corresponds to the application of a tactic which might be at a high level. Nevertheless, this helps users to examine the proof, and facilitates backtracking and alternative proof attempts.

OBJ
OBJ is based on order-sorted equational logic and is organised in parameterised modules.

ProofPower
ProofPower is a commercial implementation of HOL by ICL Secure Systems. It is being used for formal reasoning about Z specifications.

PVS
The Prototype Verification System from SRI International is an interactive system for a higher order logic with dependent types. It has its own specification language. Significant automation is achieved using decision procedures for various theories including linear arithmetic.

RRL
Rewrite Rule Laboratory is a theorem prover for first-order logic with an emphasis on equational reasoning.

SDVS
The State Delta Verification System is a verification system that incorporates simplifiers, decision procedures and symbolic execution. It is based on a temporal logic and has been mainly used for verification of computer descriptions written in languages such as Ada and VHDL.

Veritas
Veritas is a logic developed by Keith Hanna to support formal design methods. It is motivated by Martin-Löf's intuitionistic (constructive) type theory: it is higher order and provides dependent types and subtypes, but it is a classical rather than a constructive logic. The Veritas-90 version is implemented in both Standard ML and Haskell. The intention behind the implementation in the purely-functional language Haskell is to enable parallel evaluation. As in HOL, abstract data types are used to securely implement the various syntactic categories of the logic, but in addition to terms and theorems being implemented in this way, so is the representation of theories, which are first-class objects in Veritas. In HOL, theories are structures that are modified imperatively. In Veritas, a purely-functional view is taken.

  Long-term projects
HOL
Isabelle




Links
Lab Publications
Technical Reports
Search
Haiku
Last modified on Wed May 9 23:10:48 BST 2012 by ns441 | Privacy policy