Издательство Cambridge University Press, 1987, -316 pp.
Growing numbers of computer scientists recognise the importance of formal methods of system design [48]. LCF and ML are often mentioned, seldom understood. There is a wide literature, as the bibliography attests. Gordon, Milner, and Wadsworth [41] describe Edinburgh LCF, with a few remarkable examples. The present book aims to make Cambridge LCF accessible to a wide audience.
Serious students of LCF are of several kinds. Some would like an introduction to formal reasoning about computable functions. Others are interested in the principles of the machine implementation. And a few want to perform large proofs in Cambridge LCF, and require a comprehensive description.
Cambridge LCF is not the answer to all problems in formal methods. Like Edinburgh LCF its conce is denotational semantics, domain theory, and functional programming. Related systems support other formal methods, but none supports Z, VDM, CSP, CCS, or Hoare-style verification. Some 'formal' methods lack a precise meaning, making machine implementation impossible. However the goal of formal methods — introducing rigor into computer system design — can be achieved in LCF.
I Preliminaries
Survey and History of LCF
Formal Proof in First Order Logic
A Logic of Computable Functions
Structural Induction
II Cambridge LCF
Syntactic Operations for PPA
Theory Structure
Axioms and Inference Rules
Tactics and Tacticals
Rewriting and Simplification
Sample Proofs
Growing numbers of computer scientists recognise the importance of formal methods of system design [48]. LCF and ML are often mentioned, seldom understood. There is a wide literature, as the bibliography attests. Gordon, Milner, and Wadsworth [41] describe Edinburgh LCF, with a few remarkable examples. The present book aims to make Cambridge LCF accessible to a wide audience.
Serious students of LCF are of several kinds. Some would like an introduction to formal reasoning about computable functions. Others are interested in the principles of the machine implementation. And a few want to perform large proofs in Cambridge LCF, and require a comprehensive description.
Cambridge LCF is not the answer to all problems in formal methods. Like Edinburgh LCF its conce is denotational semantics, domain theory, and functional programming. Related systems support other formal methods, but none supports Z, VDM, CSP, CCS, or Hoare-style verification. Some 'formal' methods lack a precise meaning, making machine implementation impossible. However the goal of formal methods — introducing rigor into computer system design — can be achieved in LCF.
I Preliminaries
Survey and History of LCF
Formal Proof in First Order Logic
A Logic of Computable Functions
Structural Induction
II Cambridge LCF
Syntactic Operations for PPA
Theory Structure
Axioms and Inference Rules
Tactics and Tacticals
Rewriting and Simplification
Sample Proofs