Rob Nederpelt (The Netherlands Technische Universiteit Eindhoven), Herman Geuvers (Radboud Universiteit Nijmegen)

Type Theory and Formal Proof

• Gebundenes Buch

Produktbeschreibung

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.

---

Hinweis: Dieser Artikel kann nur an eine deutsche Lieferadresse ausgeliefert werden.

Produktdetails

• Verlag: Cambridge University Press
• Seitenzahl: 466
• Erscheinungstermin: 14. März 2016
• Englisch
• Abmessung: 250mm x 175mm x 29mm
• Gewicht: 1028g
• ISBN-13: 9781107036505
• ISBN-10: 110703650X
• Artikelnr.: 40742677

Autorenporträt

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.