(vai Frank, in the discussion group)
Proofs and Types by JeanYves Girard, translated and with appendices by Yves Lafont and Paul Taylor, 1989.
Based on a short graduate course on typed lambdacalculus given at the Université Paris VII in the autumn term of 19867.
An very interesting book that has gone out of print and is now available online.
A taste of the topics discussed in this smorgasbord: The CurryHoward Isomorphism, Strong Normalisation, System F, Provably Total Functions and more!
Posted to theory by Ehud Lamm on 10/7/03; 11:30:26 AM
