Book contents
- Frontmatter
- Contents
- Foreword
- Preface
- Acknowledgements
- Greek alphabet
- 1 Untyped lambda calculus
- 2 Simply typed lambda calculus
- 3 Second order typed lambda calculus
- 4 Types dependent on types
- 5 Types dependent on terms
- 6 The Calculus of Constructions
- 7 The encoding of logical notions in λC
- 8 Definitions
- 9 Extension of λC with definitions
- 10 Rules and properties of λD
- 11 Flag-style natural deduction in λD
- 12 Mathematics in λD: a first attempt
- 13 Sets and subsets
- 14 Numbers and arithmetic in λD
- 15 An elaborated example
- 16 Further perspectives
- Appendix A Logic in λD
- Appendix B Arithmetical axioms, definitions and lemmas
- Appendix C Two complete example proofs in λD
- Appendix D Derivation rules for λD
- References
- Index of names
- Index of definitions
- Index of symbols
- Index of subjects
Preface
Published online by Cambridge University Press: 05 November 2014
- Frontmatter
- Contents
- Foreword
- Preface
- Acknowledgements
- Greek alphabet
- 1 Untyped lambda calculus
- 2 Simply typed lambda calculus
- 3 Second order typed lambda calculus
- 4 Types dependent on types
- 5 Types dependent on terms
- 6 The Calculus of Constructions
- 7 The encoding of logical notions in λC
- 8 Definitions
- 9 Extension of λC with definitions
- 10 Rules and properties of λD
- 11 Flag-style natural deduction in λD
- 12 Mathematics in λD: a first attempt
- 13 Sets and subsets
- 14 Numbers and arithmetic in λD
- 15 An elaborated example
- 16 Further perspectives
- Appendix A Logic in λD
- Appendix B Arithmetical axioms, definitions and lemmas
- Appendix C Two complete example proofs in λD
- Appendix D Derivation rules for λD
- References
- Index of names
- Index of definitions
- Index of symbols
- Index of subjects
Summary
Aim and scope
The aim of the book is, firstly, to give an introduction to type theory, an evolving scientific field at the crossroads of logic, computer science and mathematics. Secondly, the book explains how type theory can be used for the verification of mathematical expressions and reasonings.
Type theory enables one to provide a ‘coded’ version – i.e. a full formalisation – of many mathematical topics. The formal system underlying type theory forces the user to work in a very precise manner. The real power of type theory is that well-formedness of the formalised expressions implies logical and mathematical correctness of the original content.
An attractive property of type theory is that it becomes possible and feasible to do the encoding in a ‘natural’ manner, such that one follows (and recognises) the way in which these subjects were presented originally. Another important feature of type theory is that proofs are treated as first-class citizens, in the sense that proofs do not remain meta-objects, but are coded as expressions (terms) of the same form as the rest of the formalisation.
The authors intend to address a broad audience, ranging from university students to professionals. The exposition is gentle and gradual, developing the material at a steady pace, with ample examples and comments, cross-references and motivations. Theoretical issues relevant for logic and computer science alternate with practical applications in the area of fundamental mathematical subjects.
- Type
- Chapter
- Information
- Type Theory and Formal ProofAn Introduction, pp. xv - xxviPublisher: Cambridge University PressPrint publication year: 2014