Reddit mentions of Lectures on the Curry-Howard Isomorphism (Volume 149) (Studies in Logic and the Foundations of Mathematics (Volume 149))

If you're truly interested in plumbing the depths of the correspondence, I'd suggest taking a look at Sørensen & Urzyczyn which gives a good deal of discussion on not only how things correspond, but also on when and how they do not (or do not in the way expected). If you're unable to shell out for the excellent book (or are unwilling to support Elsevier), I just found an online copy of an earlier version which, though not as complete, probably contains much of the same wisdom.

That's actually some good advice, which I kinda took when finding my way. More precisely, I started head first with the theory for the Curry-Howard-Lambek correspondence. While I was almost comfortable with Lambek's part, at least to begin with, I started reading more on lambda calculus and proof theory, including all the technical intricacies of completeness, undecidability, universality etc. I can even recommend the book I used, it's Sorensen and Urzyczyn's Lectures on the CH Isomorphism.

Yes, there are easier ways and more introductory books and also Barendregt's bible at the other end of the spectrum, I know. I just find it more motivating to keep in view this correspondence at all times.

I agree that it's a great book, but in my experience, it's more useful as a motivator than as a source of information. That is, after reading Girard's cryptic and tantalizing off-hand remarks, you are dying to know what on earth he is talking about.

For readers who are new to lambda calculus or proof theory, I'd recommend supplementing it with a gentler text like Sørensen and Urzyczyn's Lectures on the Curry-Howard Isomorphism (book, shorter free online version), which contains actual explanations. :)