University of Calgary

Proofs and Types

Submitted by Richard Zach on February 23, 2005 - 6:00am.

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)

GLT vs. TSI'd rate the
Submitted by Charles Stewart (not verified) on February 28, 2005 - 2:57pm.

<>GLT vs. TS<>I'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 < HREF="http://www.advogato.org/person/chalst/diary.html?start=92" REL="nofollow">[1]<>, and got into a nice discussion with Robert Solovay as a result < HREF="http://advogato.org/person/chalst/diary.html?start=96" REL="nofollow">[2]<>, which casts some light on the whole relationship between normalisation and concistency proofs that isn't, I think, widely appreciated.

<>Posted by < HREF="http://www.linearity.org/cas" REL="nofollow" TITLE="chalst@advogato.org">Charles Stewart<><>