Lambda Calculus with Types
Part of Perspectives in Logic
- Authors:
- Henk Barendregt, Radboud Universiteit Nijmegen
- Wil Dekkers, Radboud Universiteit Nijmegen
- Richard Statman, Carnegie Mellon University, Pittsburgh, Pennsylvania
- Date Published: June 2013
- availability: Available
- format: Hardback
- isbn: 9780521766142
$
94.99
Hardback
Other available formats:
eBook
Looking for an inspection copy?
This title is not currently available for inspection. However, if you are interested in the title for your course we can consider offering an inspection copy. To register your interest please contact [email protected] providing details of the course you are teaching.
-
This handbook with exercises reveals in formalisms, hitherto mainly used for hardware and software design and verification, unexpected mathematical beauty. The lambda calculus forms a prototype universal programming language, which in its untyped version is related to Lisp, and was treated in the first author's classic The Lambda Calculus (1984). The formalism has since been extended with types and used in functional programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing and verifying IT products and mathematical proofs. In this book, the authors focus on three classes of typing for lambda terms: simple types, recursive types and intersection types. It is in these three formalisms of terms and types that the unexpected mathematical beauty is revealed. The treatment is authoritative and comprehensive, complemented by an exhaustive bibliography, and numerous exercises are provided to deepen the readers' understanding and increase their confidence using types.
Read more- Presents three type disciplines using a unified framework
- Reveals many mathematical gems through the simple definitions of terms and types
- Introduces the reader to applications and includes almost 300 exercises
Reviews & endorsements
'The book has a place in undergraduate libraries because of its uniquely comprehensive, if theoretical, treatment of a timely, widely important subject. Recommended.' D. V. Feldman, Choice
See more reviews'The authors have produced a well-written, organised and comprehensive account of three important type systems. These systems' properties have been rich sources of interest to logicians for many years; their problems are not all solved, and in future work this book will almost certainly become a standard reference about them. It will also allow the more mathematically inclined computer scientist to obtain a deeper understanding of the principles behind some of the higher order languages in current use.' Bulletin of the London Mathematical Society
Customer reviews
Not yet reviewed
Be the first to review
Review was not posted due to profanity
×Product details
- Date Published: June 2013
- format: Hardback
- isbn: 9780521766142
- length: 856 pages
- dimensions: 244 x 170 x 44 mm
- weight: 1.55kg
- contains: 52 b/w illus. 300 exercises
- availability: Available
Table of Contents
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.
Related Books
Sorry, this resource is locked
Please register or sign in to request access. If you are having problems accessing these resources please email [email protected]
Register Sign in» Proceed
You are now leaving the Cambridge University Press website. Your eBook purchase and download will be completed by our partner www.ebooks.com. Please see the permission section of the www.ebooks.com catalogue page for details of the print & copy limits on our eBooks.
Continue ×Are you sure you want to delete your account?
This cannot be undone.
Thank you for your feedback which will help us improve our service.
If you requested a response, we will make sure to get back to you shortly.
×