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.
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.
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.
Inhaltsangabe
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.
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.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Shop der buecher.de GmbH & Co. KG Bürgermeister-Wegele-Str. 12, 86167 Augsburg Amtsgericht Augsburg HRA 13309
