EPSRC Reference: 
GR/H40570/01 
Title: 
COMBINING HOL WITH ISABELLE 
Principal Investigator: 
Paulson, Professor LC 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science and Technology 
Organisation: 
University of Cambridge 
Scheme: 
Standard Research (PreFEC) 
Starts: 
01 September 1992 
Ends: 
31 August 1995 
Value (£): 
122,431

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 

Related Grants: 

Panel History: 

Summary on Grant Application Form 
To exercise the technology underlying the theoremprover 'Isabelle' on major hardware/system verifications. To investigate how Isabelle compares to HOL as an environment for large proofs. To examine the use of Isabelle as an applicationoriented verification environment.Progress:The first part of the work involved comparing proofs in HOL and Isabelle. We have chosen the proofs of correctness of two hardware circuits (a parity checker and a multiplier) already described in HOL and translated them as closely as possible into Isabelle. Other examples included conjectures arising from the specification of a nuclear reactor (due to David Parnas) and theorems about Greatest Common Divisors.All these verification problems were performed in Isabelle, and they supplied us with some comparisons as to how the more applicationsoriented users view the proof process. For example, the hardware proofs involve the extensive use of rewriting; much work was invested in improving the efficiency of Isabelle's simplifier, so that now it is as fast as HOL's (and considerably more powerful).We hoped Isabelle would be particularly successful at embedding different application formalisms. We have done three different experiments along these lines; the main one concerns Lamport's Temporal Logic of Actions (TLA).Leslie Lamport developed TLA for reasoning about timing properties of concurrent programs. We have implemented TLA in Isabelle, following the calculus and mode of use described in Lamport's paper. The resulting proof system is quite usable, with few changes to the methodology and representation. We have found that Isabelle's tools (particularly the flexible parser and prettyprinting) indeed facilitate the development of embeddings. Work on TLA is continuing; we aim to perform proofs of published examples. We are also looking for other ways to improve Isabelle's support for natural and direct embeddings.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.cam.ac.uk 