Logic and computation. Interactive proof with Cambridge LCF. (English) Zbl 0645.68041

Paulson, Lawrence C.

Cambridge Tracts in Theoretical Computer Science, 2. Cambridge etc.: Cambridge University Press. XIII, 302 p.; Ł 27.50; $ 34.50 (1987).

This very interesting book concerns the interplay between logic and computation. It is about Cambridge LCF, a computer program for formal reasoning about computation, which combines methods from mathematical logic and denotational semantics.
The book consists of two parts. The first part is a more or less intuitive introduction into logic and domain theory, discussing such subjects as first-order logic, lambda calculus, computable functions, structural induction, and the inverse limit construction for recursive domains. This provides the underlying mathematics for Cambridge LCF. I found this part of the book in particular very enjoyable to read, due to the emphasis on intuition rather than formality.
The second part of the book serves as a reference manual for Cambridge LCF. It treats the syntax of the object language PP\(\lambda\), which is a mathematical language of logic and domain theory, the inference rules in LCF, its theories, tactics/tacticals and the subject of rewriting. The last chapter of the book presents several sample sessions, including proofs about the natural numbers and infinite sequences.

Reviewer: J.-J.Ch.Meyer

MSC:

68Q65	Abstract data types; algebraic specification
03-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations
68-01	Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science
03B10	Classical first-order logic
03F99	Proof theory and constructive mathematics
03D99	Computability and recursion theory
18C10	Theories (e.g., algebraic theories), structure, and semantics
03B40	Combinatory logic and lambda calculus

Keywords:

category theory; reasoning about computation; mathematical logic; denotational semantics; recursive domains; Cambridge LCF; PP\(\lambda \)

Software:

Cambridge LCF; Miranda; Nuprl; HOL