The revised edition contains a new chapter which provides an elegant description of the semantics. The various classes of lambda calculus models are described in a uniform manner. Some didactical improvements have been made to this edition. An example of a simple model is given and then the general theory (of categorical models) is developed. Indications are given of those parts of the book which can be used to form a coherent course.
I've heard much about this book, supposedly the supreme guide to rigorous type-free LC. Tales are told and ballads sung of its epic difficulty; I admit fair intimidation. It's hard to find this one for less than $100, so it's been sitting in the Amazon watch queue for quite some time now...I'd like to get a copy before next summer, so I can churn through it prior to taking CS6390 (or whatever they're calling the graduate programming language theory class these days). Supposedly, this is a great follow-up to Benjamin Pierce's books, which I found generally excellent.
update Thu Feb 26 17:54:47 EST 2009 bah this book is never going to be offered cheaply used, it seems -- usually a good portent for textbooks of repute, indicating that few owners are willing to hand their copies over. $111.23 on amazon -- a splurge to be sure, but hey there's a recession on, and we've all got to make it rain now and then for the economy.
update Mon May 18 20:07:42 EDT 2009 I can't take any more of this for at least a few months. Barendregt has put together an awe-inspiring work, but not one that's meant to be chewed through. Unfortunately, skimming seems an impossibility, given the supremely striated content -- I tried jumping 10-20 pages several times, and immediately had no idea what was going on. I was willing to give it time, but 10 chapters in or so, I haven't gained much insight; The Lambda Calculus, Volume 103 in the Studies of Logic and the Foundations of Mathematics and almost certainly the largest and best-known (heh, possibly known to about 50k people worldwide, and that's being very generous) is certainly a pillar of computing and type theory, but I'm content to trust the good Dutchman that it all works. It appears I'm never to be a category theorist; so it must, I suppose, go.
5 stars due to obvious sui generis status, and being more informative in the first two-hundred pages than the dozens of books that try to approach λ-gaming from the sidelong. I finally understand combinators on an axiomatic, theoretical level, which had always kind of bugged me (especially as my home workstation -- since being rebuilt in 2006, anyway -- has been named recombinator (although that's a reference to biocomputing rather than computation theory!)). Who am I to criticize one of the Greatest of all Time? Ἀπόδοτε οὖν τὰ Καίσαρος Καίσαρι καὶ τὰ τοῦ Θεοῦ τῷ Θεῷ.
Extremely heavy. I only read part of it, the parts that interested me the most. The book builds what seems like every aspect of lambda calculus from every different perspective, showing equivalences, similarities and differences in a very complete way. The proofs are usually good, and there was less "left to the reader" than I expected. This however, makes it super dense, and I feel a little more explanation of the idea of what it's trying to achieve or what a theorem "is supposed to mean" would be helpful. That said, the book is super big already, so there probably wouldn't be space for that.