Growing numbers of computer scientists recognise the importance of formal methods of system design [48]. LCF and ML are often mentioned, seldom understood. There is a wide literature, as the bibliography attests. Gordon, Milner, and Wadsworth [41] describe Edinburgh LCF, with a few remarkable examples. The present book aims to make Cambridge LCF accessible to a wide audience.

Serious students of LCF are of several kinds. Some would like an introduction to formal reasoning about computable functions. Others are interested in the principles of the machine implementation. And a few want to perform large proofs in Cambridge LCF, and require a comprehensive description.

Cambridge LCF is not the answer to all problems in formal methods. Like Edinburgh LCF its concern is denotational semantics, domain theory, and functional programming. Related systems support other formal methods, but none supports Z, VDM, CSP, CCS, or Hoare-style verification. Some ‘formal’ methods lack a precise meaning, making machine implementation impossible. However the goal of formal methods — introducing rigor into computer system design — can be achieved in LCF.

How to read this book

People find LCF difficult to approach because it requires familiarity with a mass of background material. The book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. Many advocates of formal methods have a lamentably weak grasp of this fundamental material. Part II describes Cambridge LCF in enough detail to serve as a reference manual, though operating instructions should be supplied with the software.