Ulteriori informazioni
Informationen zum Autor Henk Barendregt holds the chair on the Foundations of Mathematics and Computer Science at Radboud University, Nijmegen, The Netherlands. Klappentext This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification. Zusammenfassung Typed lambda calculus is used in functional programming (Haskell! Clean) and proof assistants (Coq! Isabelle! HOL)! which are used to design and verify IT products and mathematical proofs. This book reveals unexpected mathematical beauty in three classes of typing: simple types! recursive types and intersection types. Numerous exercises are provided. Inhaltsverzeichnis List of contributors; Preface; Introduction; Part I. Simple Types: 1. The simply typed lambda calculus; 2. Properties; 3. Tools; 4. Definability, unification and matching; 5. Extensions; 6. Applications; Part II. Recursive Types: 7. The systems; 8. Properties of recursive types; 9. Properties of terms with types; 10. Models; 11. Applications; Part III. Intersection Types: 12. An exemplary system; 13. Type assignment systems; 14. Basic properties; 15. Type and lambda structures; 16. Filter models; 17. Advanced properties and applications; Bibliography; Symbol index; Names index; Definitions index.
