Computation and Reasoning

• Covers all the major relevant issues
• Includes new and recent results
• Detailed explanation of applications

Readership: Computer scientists. postgraduate students in computer science, logicians (people and researchers interested in logic).

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

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