Proofs and Types

Proofs and Types, the classic 1989 proof theory text by Jean-Yves Girard (translated and with appendices by Paul Taylor and Yves Lafont) has been online for over a year, I just found out. Now that Troelstra/Schwichtenberg is around, perhaps no longer the first place you’d go to read up on the Curry-Howard isomorphism and normalization, but still very good to have around. (via EFP)

One thought on “Proofs and Types

  1. GLT vs. TSI’d rate the Girard-Lafont-Taylor text much higher as an introduction to the formulae-as-types/normalisation field than Troelstra-Schwichtenberg, for all sorts of reasons, but with the warning that Girard has an agenda and the text does not quite conform to usual standards of scholarship.I posted an advert for the GLT book on my diary a couple of years back [1], and got into a nice discussion with Robert Solovay as a result [2], which casts some light on the whole relationship between normalisation and concistency proofs that isn’t, I think, widely appreciated.Posted by Charles Stewart

Leave a Reply

Your email address will not be published. Required fields are marked *