Lectures on the Curry-Howard Isomorphism

Apparently there's a new book version of these excellent lecture notes.

Anyone see this? I'd be glad to know more about this book.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Link dead?

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

Website Reorg

With a bit of digging, I found it here.

book link

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.

That was my point...

That was my point...


Amazon Canada lists it for CDN$ 89.18 (pre-order only) - according to an online currency converter that's "only" about US$80.

Taking one for the team

I just ordered it from them (though I'm a bit skeptical on this one, since I'm still waiting for them to ship me Barendregt's LC book in the same series.)

I'll report back to LtU once I get it and get to reading it.

Finally Have It

After waiting for several months, I finally have my copy.

Review forthcoming in the next few weeks.

(Anyone else read it in the meantime?)

In lieu of a review...

...which is a big task, can you say what content has been expanded? One of the surprises, for me, of the original lecture notes was that they didn't properly tackle Prawitz's ideas about natural deduction and the meaning of propositions: for me, these ideas are the source of most of what is interesting about the correspondence. Has this been fixed?

Unnatural deductions

can you say what content has been expanded?

I'm not sure that is actually an easier task. ;-) A quick scan of the contents shows that, though the structure is substantially the same, all the sections seem to have more pages.

Quickly re-reading their summary of the LC in the original after having read that in the book shows fairly significant rewrites of the material: where the original lecture notes are a bit more discursive, the book is quite pithy, as one might expect.

they didn't properly tackle Prawitz's ideas about natural deduction and the meaning of propositions

If you give me some idea about what you found lacking, I can better assess for it when I get to the appropriate sections. ;-)

My own "test case" will be the chapter on classical logic and control: I found the original presentation unsatisfying and hope to get a deeper insight into the subject this time around.

Half-way Whole-hearted Review

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.


I agree, the link to classical logic is one of the two or three litmus-like test topics. In my doctoral dissertation I tried to combine this with the foundational issue above, but with hindsight I only partly succeeded, because the link to the programmatic aspects of scheme/ML call/cc was rather obscure. It sounds like the field is still open for a "successor account" that combines both viewpoints.

Are you aware of a pair of papers, the first by Lafont, Streicher & Reus called "Expressing implication by means of negation", and the second by Streicher & Reus that appeared in the Journal of Functional programming about 2000ish? They have been my perennial favourites as papers that use a powerful set of theoretical inisghts to cast light on the operational side.

Postscript (2009) — Refs for posterity:

  1. Y. Lafont, B. Reus, T. Streicher: Continuations Semantics or Expressing Implication by Negation (.ps). Technical Report 9321, Ludwig-Maximilians-Universität, München, 1993. It was from the proceedings of some obscure workshop, IIRC.
  2. T. Streicher, B. Reus: Classical logic: Continuation Semantics and Abstract Machines (.ps.gz). Journal of Functional Programming. Vol 8(6), pp. 543-572, 1998. Link is to much older preprint, not version that JFP published.

Lectio longa, vita brevis...

Are you aware of a pair of papers

Thanks for the reference: I'll put them in my queue.

(Your dissertation is already there. ;-) )

link to book

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

Strange to see this at Walmart ...

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."

Online booksellers

including walmart.com, will list virtually any book that is published by a major publishing house, and quite a few that aren't. ATTAPL is also easily found at walmart.com, I just tried it.

Walmart.com's online book service is not limited to the general-interest stuff that is stocked in their stores. (Don't expect to see PLT texts on the shelf of your nearest Wal-Mart store).