The Λ-calculus lies at the very foundations of Computer Science. Besides its historical role in compatibility 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 Λ-calculus. The first six chapters concern this calculus and cover the basic theory, reduction, models, computability and the relationship between the Λ -calculus and Combinatoryh Logic. Chapter 7 presents a variety of typed calculi; first the simply typed Λ-calculus, then Milner-style...