The Lambda Calculus: Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics) [Paperback]

This book itself is purely theoretical and principally aimed for researchers/students of its field.

This book is very comprehensive. In fact, this book successfully compiles almost all results on type-free lambda-calculus up to the time of its publication (early 1980's).

Surprisingly enough!, however, this very technical encyclopedic monograph is self-contained.

Proofs of all theorems/lemmata are given up to details except for cases that they are intentionally left for excercises.

Therefore, even a novice of its field can follow all of the proofs. The only one thing that such a novice must have is patience. His/her patience will surely be rewarded.

Backgrounds assumed in this encyclopedic monograph is the very beginning level understanding of mathematical logic. If you are not familiar with math logic, you can learn the necessary backgrounds with any introductory textbooks on math logic.

All more technical notions and notations are defined/explained in this book. Many interesting examples are given.

Exercises at the end of each charpter are very helpful and also are very interesting. The author clearly paid much attention and took care on the arrangement of exercises so that readers can tackle easier one at first. Moreover such carefully arranged exercises tell readers more. Readers will understand very delicate but important points during solving exercises by themselves. In other words, the last sentence means the following fact: imagine there are two intuitively similar notions
(it is often the case that very abstract theory has many such pairs of notions) that novices can confuse each other. Solving one exercise tell the novice that one notion is not implied from the other. Also solving another exercise tell vice-versa.

Indices and references are very useful. In fact, indices are carefully designed. Not only the index of technical terms, there are indices for symbols and authors (of references refered in the main text). References are very comprehensive.

There are very few typos (another surprising points! Math books almost always handreds of typos) except for misuses of type-faces which are clearly due to typesetting by the publisher.

This book, as I pointed before, is on pure math logic and its readership is clearly researchers/students of its field.

But, as a computer scientist, I recommend this book to all of the functional programmers, who, at least, are serious about the background of their profession.

If you read this book, you will understand that there is a very beautiful (though abstract) world of theories behind ML/Haskell programming.

If you are a student who wants study lambda-calculus, combinatory logic, type theory, constructive math, etc.,
then, this book is for you, too, of course.
This encyclopedia doubtlessly will give you the basis to become the researcher on such fields.