[TYPES/announce] Newly Published book, Lambda Calculus with Types

[Katy Strong]

New Book Published by

Henk Barendregt, Radboud Universiteit Nijmegen
Wil Dekkers, Radboud Universiteit Nijmegen
Richard Statman, Carnegie Mellon University, Pittsburgh, Pennsylvania

Lambda Calculus with Types

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

Hardback ISBN-13: 9780521766142
Perspectives in Logic Series
USD 90.00, GBP 60.00

Also Available as an e-book

For more information, please visit: www.cambridge.org/9780521766142