Computation and reasoning: a type theory for computer science

Abstract

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