**A couple of links**

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.