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.
Reviewer: J.-J.Ch.Meyer


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
Full Text: DOI