che-chandler.de
Type Theory and Formal Proof
HC gerader Rücken kaschiert
Print on Demand | Lieferzeit: Print on Demand - Lieferbar innerhalb von 3-5 Werktagen I
Alle Preise inkl. MwSt. | Versandkostenfrei
Nicht verfügbar
Zum Merkzettel
Gewicht:
979 g
Format:
250x175x29 mm
Beschreibung:
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.
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.
A gentle introduction for graduate students and researchers in the art of formalizing mathematics on the basis of type theory.