(vai Frank, in the discussion group)
Proofs and Types by Jean-Yves Girard, translated and with appendices by Yves Lafont and Paul Taylor, 1989.
Based on a short graduate course on typed lambda-calculus given at the Université Paris VII in the autumn term of 1986-7.
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 Curry-Howard Isomorphism, Strong Normalisation, System F, Provably Total Functions and more!
Posted to theory by Ehud Lamm on 10/7/03; 11:30:26 AM