Lawrence C. Paulson and Michael J. C. Gordon
Computer Laboratory, University of Cambridge
Funded by the EPSRC (1 Sep 1992 - 31 Aug 1995).
Grant reference GR/H40570. Value £122,431
HOL is a theorem prover for higher-order logic. Since 1984 it has been used for a series of demanding proofs, mainly for hardware verification. Isabelle is a generic theorem prover; it can handle higher-order logic, set theory, and many other logics. It is of much more recent design and is yet to be tested on really large examples.
HOL and Isabelle are based on many of the same principles. However, Isabelle also provides support for unification and embedded logics, and could provide a better environment for large proofs than HOL. We propose to investigate whether this really is the case. We shall evaluate Isabelle on major hardware/system verifications.
Task-specific tools are often better than generic ones. However, generic tools based on new technology may easily have the edge: automatically generated LR(1) parsers are usually better than hand-coded parsers. Researchers at Chalmers Univeristy adopted Isabelle to do proofs in Constructive Type Theory [2] when one might have expected them to prefer Nuprl, which supports this logic specifically.
While performing the proofs, we expect limitations of Isabelle to appear and plan to correct them whenever possible. We also expect that aspects of the HOL methodology will have to be modified when using Isabelle. We do not expect that Isabelle will turn out to be useless for hardware verification; but in this event, we shall diagnose the problem and begin to design a system combining the advantages of HOL and Isabelle.
In short, we propose to exploit the skill and experience of the HOL community to exercise the technology of Isabelle and to improve its implementation.
HOL [1] is an interactive theorem prover for higher-order logic. Descended from Cambridge LCF, it supports forwards and backwards proof in the LCF style. HOL has been used for many different kinds of theorem proving tasks. For example, at the last HOL Users Meeting (held at the University of California in Davis during September 1991) work was presented on using HOL for representing CCS, reasoning about VHDL, reasoning about finite state machines, modelling real time systems, reasoning within the Temporal Logic of Actions, compiler correctness, program verification, program transformation/refinement, and reasoning about Petri nets. Many of these applications use embeddings of special purpose formalisms in higher order logic.
Isabelle is a generic theorem prover [4,5]. It supports interactive proof in several formal systems, including first-order logic (intuitionistic and classical), modal logic, Martin-Löf type theory, and Zermelo-Fraenkel set theory. New logics can be introduced by specifying their syntax and rules of inference; little or no programming is required. Both natural deduction and sequent calculi are allowed.
The latest version of Isabelle, called Isabelle-91, allows the meta-level type system to perform automatic type checking in object-logics. This works especially well for many-sorted logics and higher-order logic. Isabelle-91's version of higher-order logic is virtually identical (as a formal system) to the higher-order logic implemented by HOL. Isabelle has proved deep theorems in higher-order logic, such as the Schröder-Bernstein Theorem and the Well-founded Recursion Theorem. We want to investigate whether Isabelle can handle real verifications involving many large theorems.
Isabelle and HOL have many features in common. Both are written in some dialect of ML. Both rely upon ML's type checking for soundness. Both can be extended by users, programming in ML. Both provide tactics and tacticals, and other tools for proving theorems.
Unlike HOL, Isabelle provides direct support for unification. Its data structure for terms includes a class of variables that stand for unknowns. Such variables may be instantiated during a proof. In hardware proofs, they could allow timing details to be omitted from goals; the exact number of gate delays would be determined by the proof. Unification underlies Isabelle's predicate calculus proof procedures, which can prove quite complicated formulae.
Much recent work in HOL involves embedded logics. To embed a logic, the semantics of each symbol is expressed in higher-order logic. As a generic theorem prover, Isabelle should be particularly well suited for supporting embedded logics. Its parser/pretty-printer generator makes it easy to define the syntax; tactics and derived rules can be constructed without programming.
HOL has many powerful tools of its own, such as Melham's datatype definition package [3]. Large HOL proof libraries also exist. Adding these facilities to Isabelle is mainly a matter of labour. In contrast, adding Isabelle's facilities to HOL would seem to require a fundamental redesign of HOL.
There are currently two SERC supported projects that use HOL: the SAFEMOS project and the HOL-ELLA project. These are both funded under the IED programme. Both projects are in their second (of three) years.
The SAFEMOS project is joint with Inmos, SRI International and Oxford Programming Research Group and aims to build a verified compiler for a verified processor. A simple real-time programming language, called Safe, has been defined and a compiler for it verified. A processor for the target language has also been designed and verified. All the proofs are done in HOL.
The HOL-ELLA project is investigating the semantic embedding of the ELLA simulation language in HOL. A subset of ELLA has been selected and a formal semantics for it given. Using this semantics, a prototype verification system for ELLA has been implemented on top of HOL. This is currently being tested. It is hoped to use the Safe processor as the main example for testing the HOL-ELLA system.
We expect both these projects to be a source of challenging examples for testing the HOL application of Isabelle.
The programme of work is simple. We shall perform increasingly difficult HOL proofs in Isabelle in order to identify any difficulties as early as possible. The first proof will probably be the correctness of a self-timed sequential multiplier.
We do not wish merely to check that Isabelle can perform the same proofs as HOL; we would like to demonstrate that Isabelle supports a higher level of proof. We intend to take advantage of Isabelle's facilities to simplify existing proofs as much as possible. In particular, (i) we expect to demonstrate that Isabelle's unification-based approach to theorem proving is more effective than HOL's and (ii) we plan to use Isabelle's capability for simultaneously supporting several interconnected formalisms to improve on HOL's treatment of semantic embedding.
HOL has many features designed for hardware verification --- for example, a syntax for bit strings. Because Isabelle is a generic theorem prover, we shall resist the temptation to add features to its version of higher-order logic; whenever possible, we shall instead strengthen the logic-independent part of Isabelle. Note that these are not just programming problems, but fundamental issues in the notion of ``logic.''
Some time may be spent investigating alternative logics for formal reasoning, such as set theory. The type system of higher-order logic catches many errors, but sometimes it is a straightjacket. Set theory is typeless and may be easier to use in such situations.
Sara Kalvala has some experience with building user interfaces for HOL, based on X-Windows. If time permits, she will produce a user interface for Isabelle, with emphasis on supporting large proofs.
Hardware verification has already attracted much interest from industry. Several companies, including ICL, Hewlett Packard and Inmos, are using HOL. Isabelle may turn out to be even better than HOL for hardware verification, for reasons discussed above. We intend to evaluate and strengthen Isabelle's treatment of ``industrial size'' proofs.