The lambda-calculus lies at the very foundations of computer
science. Besides its historical role in computability theory it has
had significant influence on programming language design and
implementation, denotational semantics, and domain theory. The book
emphasises the proof theory for the type-free lambda-calculus. The
first six chapters concern this calculus and cover the basic theory,
reduction, models, computability, and the relationship between the
lambda-calculus and combinatory logic. Chapter 7 presents a variety
of typed calculi; first the simply typed lambda-calculus,...