Lambda the Ultimate

I've just skimmed it; it seems to be a decent elementary introduction to some of the most important topics, and I expected it to be stronger on the history of the topic than it is. Section 3.1, treating HM-style typing, was solid. I saw that Scott's D_infinity model was treated, in section 4.1: while the fact of the model's existence is certainly of interest, it doesn't seem very `core' to CL, and seemed like an odd inclusion for this article. It maybe that the author's emphasis on self-application led her to want to show how a mathematical model could handle it.

Overall, there's not much here for someone who has done a thorough course on the lambda calculus, but it's probably a good reference for non-specialists who might want to get the idea of what calculi of higher-order functions are about. It falls short of being a good introduction to CL for lambda-calculus hackers: that would still be Hindley & Seldin.

I note that Barendregt & Klop are slated to write an article on the lambda calculus.

I skimmed it too.

I would find it really nice if some basic complexity results would be included at the right places (like the expansion of Shoenfinkel of FOL is O(n^3), I think. That can easily be included.)

I expected also to see an exposition of deduction styles [sequent calculi / resolution] for CL's with/and some computational results like Knuth-Bendix completion but I gather that doesn't fall into the current understanding of the CL field.

To sum it up: more computational logic results!