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

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.

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 |