Cambridge LCF is a computer program for reasoning about computation. It combines the methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of program statements. Cambridge LCF is based on an earlier theorem-proving system called Edinburgh LCF, which introduced a design that gives the user complete flexibility to use and extend the system. A goal of this book is to explain that design, which has been adopted in several other systems.
The book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. These are explained at an intuitive level, giving references to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach.
Most features of ML (including modules and imperative programming) are covered in depth and the book can be used without an ML reference manual. The reader 1s assumed to have some experience in programming in conventional languages such as C or Pascal. For such individuals, be they students, graduates or researchers, this will be a convincing introduction to functional programming.