Computation and Reasoning
A Type Theory for Computer Science
- Description
- Features
- Contents
- Authors
- Reviews
- Lecturer Resources
- Teacher Resources
- Student Resources
- Sample Pages
- ebook
This book develops a new type theory and shows how it can be applied to computer science, in particular to the effective development of programs and proofs.
Preface
Introduction
1. The extended calculus of constructions
2. Basic meta-theoretic properties
3. Strong normalisation
4. The internal logic and decidability
5. A set-theoretic model
6. Computational and logical theories
7. Specification and development of programs
8. Towards a unifying theory of dependent types
Bibliography
Notation and symbols
Index
Zhaohui Luo , Lecturer/Research Fellow, Department of Computer Science, JCMB, Edinburgh
`a comprehensive account of ... one particular type theory, The Extended Calculus of Constructions ... I found this to be a well written, thorough and enjoyable account of the ECC ... I recommend Computation and Reasoning wholeheartedly.'
The Computer Journal, Vol 37, No 6, 1994 |d 17/08/1995