13 Oct 2003 chalst   » (Master)

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.

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!