Lambda the Ultimate

The link seems to be dead, but this one seems to be what you were referring to: http://citeseer.ist.psu.edu/519604.html

Following is the amazon link.

The PDF notes are 273 pages, while the book apparently has 456 pages! The extra pages (and printed copy) come in at about $120 though. Perhaps someone can review it here.

I've gotten about half way through this book, and have enough of a sense of it to offer my promised review.

This book covers the basics of proof theory, logic, lambda calculus and type theory through the disciplined focus bringing out the relationships between them.

Compared to the original lecture notes, I find the book much more disciplined and cohesive. They seem to have rewritten the sections so that as you move through the different topics, the very presentation helps to bring out the parallels and relationships between them: the actual isomorphism becomes almost a formality.

Much of the material will be familiar to someone already well-read in the subject areas, but the focused and pithy writing style and the methodical presentation will likely make this a good reference work, and very nice refresher as well. With its plethora of excercises, backed up by hints and soltions at the back of the book, this would be an excellent source for a graduate course or graduate self-study.

Again to compare with the freely available lecture notes, my litmus-test section was the chapter on classical logic and control operators, and I found this to be much superior to the original. Like much of the book, it seems to have been re-written for clarity, and they have refined the lambda calculus they use to one which makes more plain what is going on. I got out of it what I'd hoped: much improved intuitions about what the correspondence between classical logic and control operators actually means and how it works.

I should make a few comments about what this book is not. It is not an undergraduate level book. The presentation is very focused, methodical and disciplined, as I've said, and this means that it leaves out a lot of the hand-holding explanation a truly "beginner-level" book would leave out. However, there is enough motivating commentary so that an experienced reader of such material never finds himself asking "Why should I care about this again?", as can sometimes happen.

Likewise, this is not an encyclopedic coverage of the subject areas: at all times the authors keep focus and give a solid presentation of all the relevant and standard aspects of the material, but never lose sight of their goal of tying each area together. As a result, they don't spend any time digressing into rabbit-holes along the way that might be of interest to specialists in that area, which might dissappoint some, but I think overall is a massive strength.

The only subject matter that might not be so obviously relevant or standard is their presentation of Lorenzen dialogues, a kind of game semantics, for each of the propositional logics. (This seems to be new to the book.) I found this material quite interesting, but was less sure how it fit in with everything else, though it does present a fairly intuitive model of how proofs are computational; perhaps that's why its there.

At this point I might as well cut to the chase: is this book worth its hefty price tag? For some, no book could be good enough to pay that kind of money, especially when a reasonably good free alternative exists.

For myself, I'm enjoying reading it, strengthening my relevant intuitions, and will likely refer back to it as a reference in the future, so I have no regrets whatsoever about supporting the authors and the publishing company who have obviously worked so hard to produce such an excellent work on a subject that is near and dear to LtUers hearts.

If find any surprises, good or bad, in the second half of the book, I'll post here again.

It took me a minute to find the book online, so for others, here it is on the publishing company's site.

The price is still better at Amazon (currently about US $97 versus $103), but it sure is odd to see this book listed at Walmart, given their reputation for catering to the broadest possible markets.

"Thank you for shopping at Walmart — and watch out for impredicativities in your type theory on the way out."