This book gives an account of combinatory logic and lambda-calculus models.This book gives an account of combinatory logic and lambda-calculus. The grammar and basic properties of both systems are discussed, followed by explanations of type-theory and lambda-calculus models. The treatment is as non-technical as possible with many examples and exercises.This book gives an account of combinatory logic and lambda-calculus. The grammar and basic properties of both systems are discussed, followed by explanations of type-theory and lambda-calculus models. The treatment is as non-technical as possible with many examples and exercises.Combinatory logic and lambda-calculus, originally devised in the 1920s, have since developed into linguistic tools, especially useful in programming languages. The authors previous book served as the main reference for introductory courses on lambda-calculus for over 20 years: this long-awaited new version is thoroughly revised and offers a fully up-to-date account of the subject, with the same authoritative exposition. The grammar and basic properties of both combinatory logic and lambda-calculus are discussed, followed by an introduction to type-theory. Typed and untyped versions of the systems, and their differences, are covered. Lambda-calculus models, which lie behind much of the semantics of programming languages, are also explained in depth. The treatment is as non-technical as possible, with the main ideas emphasized and illustrated by examples. Many exercises are included, from routine to advanced, with solutions to most at the end of the book.Preface; 1. The ?-calculus; 2. Combinatory logic; 3. The power of ? and CL; 4. Computable functions; 5. Undecidability; 6. Formal theories; 7. Extensionality in ?-calculus; 8. Extensionality in CL; 9. Correspondence between ? and CL; 10. Simple typing, Church-style; 11. Simple typing, Curry-style in CL; 12. Simple typing, Curry-style in ?; 13. Generalizations of typing; 14. Models of CL; 15. Ml£®