Logic and computation : interactive proof with cambridge LCF / Lawrence C.Paulson.
Material type:
TextSeries: Cambridge tracts in theoretical computer science ; 2 Publication details: Cambridge : Cambridge University Press, 1990.Description: xiii, 302 p. : ill. ; 25 cmISBN: - 9780521395601
- 005.1 23 P332
| Item type | Current library | Call number | Status | Date due | Barcode | Item holds | |
|---|---|---|---|---|---|---|---|
| Books | ISI Library, Kolkata | 005.1 P332 (Browse shelf(Opens below)) | Available | C26347 |
Includes bibliographical references and index.
1. Survey and history of LCF--
2. Formal proof in first order logic--
3. A logic of computable functions--
4. Structural induction--
5. Syntactic operations for PP--
6. Theory structure--
7. Axioms and inference rules--
8. Tactics and tacticals--
9. Rewriting and simplification--
10. Sample proofs--
Bibliography--
Index.
The book is based in part on the author's own research as well as on graduate teaching. Thus it can be used to accompany courses on hardware verification and as a resource for research workers.
There are no comments on this title.
