J. Girard, Y. Lafont, and P. Taylor. Cambridge Tracts in Theoretical Computer Science Cambridge University Press, (1989)This is textbook on proof theory and type systems, based on lectures by Girard. It contains an appendix by Lafont on linear logic, and also treats Girard's polymorphic lambda calculus..