Skip to content
Register Sign in Wishlist

Lambda Calculus with Types

$90.95 (C)

Part of Perspectives in Logic

Fabio Alessi, Henk Barendregt, Mark Bezem, Felice Cardone, Mario Coppo, Wil Dekkers, Mariangiola Dezani-Ciancaglini, Gilles Dowek, Silvia Ghilezan, Furio Honsell, Michael Moortgat, Paula Severi, Richard Statman, Pawel Urzyczyn
View all contributors
  • Date Published: July 2013
  • availability: Available
  • format: Hardback
  • isbn: 9780521766142

$ 90.95 (C)

Add to cart Add to wishlist

Other available formats:

Looking for an examination copy?

This title is not currently available for examination. However, if you are interested in the title for your course we can consider offering an examination copy. To register your interest please contact providing details of the course you are teaching.

Product filter button
About the Authors
  • 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.

    • 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
    Read more

    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

    "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

    See more reviews

    Customer reviews

    Not yet reviewed

    Be the first to review

    Review was not posted due to profanity


    , create a review

    (If you're not , sign out)

    Please enter the right captcha value
    Please enter a star rating.
    Your review must be a minimum of 12 words.

    How do you rate this item?


    Product details

    • Date Published: July 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
    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
    Symbol index
    Names index
    Definitions index.

  • Authors

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

    Wil Dekkers, Radboud Universiteit Nijmegen
    Wil Dekkers is an Associate Professor in the Institute of Information and Computing Sciences at Radboud University, Nijmegen, The Netherlands.

    Richard Statman, Carnegie Mellon University, Pittsburgh, Pennsylvania
    Richard Statman is a Professor of Mathematics at Carnegie Mellon University, Pittsburgh, USA.


    Fabio Alessi, Henk Barendregt, Mark Bezem, Felice Cardone, Mario Coppo, Wil Dekkers, Mariangiola Dezani-Ciancaglini, Gilles Dowek, Silvia Ghilezan, Furio Honsell, Michael Moortgat, Paula Severi, Richard Statman, Pawel Urzyczyn

Sorry, this resource is locked

Please register or sign in to request access. If you are having problems accessing these resources please email

Register Sign in
Please note that this file is password protected. You will be asked to input your password on the next screen.

» Proceed

You are now leaving the Cambridge University Press website. Your eBook purchase and download will be completed by our partner Please see the permission section of the catalogue page for details of the print & copy limits on our eBooks.

Continue ×

Continue ×

Continue ×
warning icon

Turn stock notifications on?

You must be signed in to your Cambridge account to turn product stock notifications on or off.

Sign in Create a Cambridge account arrow icon

Find content that relates to you

Join us online

This site uses cookies to improve your experience. Read more Close

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.

Please fill in the required fields in your feedback submission.