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)
posted by Richard Zach @ 11:00 PM
1 Comments
Links to this post
1 Comments:
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
Post a Comment
Links to this post:
Create a Link
<< Home