In the discussion about appropriate consequence relations for doing proof- checking that was discussed here almost a year ago, raph asked me if I could recommend an online source to the theory of the polymorphic lambda-calculus. I couldn't, but I suggested the Girard-Lafont-Taylor book as the best offline reference. Some news: the book has gone out of print, and Paul Taylor has made the full text of Proofs and Types available online. So now no-one has any excuse for not knowing why strong normalisation of the polymorphic lambda calculus is equivalent to the 1-consistency of second-order arithmetic...
Also available online, is a tutorial by two of my colleagues, Alessio Guglielmi and Paola Bruscoli, on the Proof Theoretic Foundations of Logic Programming.
Update: Following a comment by solovay, I've tightened the above statement relating Z2 to system F. There's more in this diary entry.