Rob Nederpelt was Lecturer in Logic for Computer Science until his retirement. Currently he is a guest researcher in the Faculty of Mathematics and Computer Science at Eindhoven University of Technology, The Netherlands.

Klappentext

A gentle introduction for graduate students and researchers in the art of formalizing mathematics on the basis of type theory.

Zusammenfassung
Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This book provides a gentle step-by-step introduction in the art of formalizing mathematics on the basis of type theory. It is suitable for a broad audience, ranging from undergraduate students to researchers.

Inhalt

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 technical notions; Index of defined constants; Index of subjects.