home > book reviews > Lawrence C. Paulson
Google > Lawrence C. Paulson


Books

Short works

Books : reviews

Lawrence C. Paulson.
Logic and Computation: Interactive proof with Cambridge LCF.
CUP. 1987

This book is concerned with techniques for formal theorem proving, with particular reference to Cambridge LCF (Logic for Computable Functions).

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.

Lawrence C. Paulson.
ML for the Working Programmer.
CUP. 1991

This book teaches the methods of functional programming – in particular, how to program in Standard ML, a functional language recently developed at Edinburgh University. The author shows how to use such concepts as lists, trees, higher-order functions and infinite data structures and includes a chapter on formal reasoning about functional programming. However this is a book designed to be used; the author avoids dogma, emphasises efficiency and provides many practical and interesting programs. These include fast sorting functions and efficient functional implementations of arrays, queues and priority queues. Large examples include a λ-calculus reducer and a theorem prover.

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.