Proof-theory

Jean Yves Girard has two textbooks on the web :

Jean Yves Girard, Yves Lafont and Paul Taylor: Proofs and types (175 p.).
("Based on a short graduate course on typed lambda-calculus given at the Université Paris VII in the autumn term of 1986-7")

Jean Yves Girard: The blind spot (.pdf , 500 p.)
(Complete english version of a book to be published soon (in french) - From Lectures on proof-theory, Roma Tre, October-December 2004 ).