Henk Barendregt (Radboud Universiteit Nijmegen), Wil Dekkers (Radboud Universiteit Nijmegen), Richard Statman

Lambda Calculus with Types

• Gebundenes Buch

Produktbeschreibung

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.

Produktdetails

• Perspectives in Logic
• Verlag: Cambridge University Press
• Seitenzahl: 856
• Erscheinungstermin: 11. Juni 2014
• Englisch
• Abmessung: 250mm x 175mm x 50mm
• Gewicht: 1614g
• ISBN-13: 9780521766142
• ISBN-10: 0521766141
• Artikelnr.: 33154149

Autorenporträt

Henk Barendregt holds the chair on the Foundations of Mathematics and Computer Science at Radboud University, Nijmegen, The Netherlands.

Inhaltsangabe

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.